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 wulflinc5 THE 2005-04-21 00:25:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=19720 boxname=wulflinc5 idbench=1517 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4f5f6e30a602f3968daa9ca41c7da043 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb IDLAUNCH: 19720 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 441360 kB Buffers: 39272 kB Cached: 528636 kB SwapCached: 2272 kB Active: 220176 kB Inactive: 352868 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 441108 kB SwapTotal: 2097136 kB SwapFree: 2094864 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6940 kB Slab: 14468 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 00:45:40 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 19720 7 1200.21 10 #### 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.84 0.95 0.90 2/54 12941 Raw data (stat): 12941 (runsolver) R 12940 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482522525 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0011 s] Raw data (loadavg): 0.87 0.95 0.90 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2051 0 0 0 994 4 0 0 25 0 1 0 482522525 10203136 2026 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2491 2026 603 41 0 2450 0 vsize: 9964 [startup+20.0023 s] Raw data (loadavg): 0.89 0.95 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2380 0 0 0 1992 6 0 0 25 0 1 0 482522525 11542528 2355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2818 2355 603 41 0 2777 0 vsize: 11272 [startup+30.003 s] Raw data (loadavg): 0.90 0.95 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2486 0 0 0 2992 6 0 0 25 0 1 0 482522525 11948032 2461 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2917 2461 603 41 0 2876 0 vsize: 11668 [startup+40.0032 s] Raw data (loadavg): 0.92 0.95 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2486 0 0 0 3991 7 0 0 25 0 1 0 482522525 11948032 2461 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2917 2461 603 41 0 2876 0 vsize: 11668 [startup+50.0035 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2486 0 0 0 4991 7 0 0 25 0 1 0 482522525 11948032 2461 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2917 2461 603 41 0 2876 0 vsize: 11668 [startup+60.0033 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 2827 0 0 0 5990 8 0 0 25 0 1 0 482522525 13287424 2802 4294967295 134512640 134672761 3221224544 3221223728 134558632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3244 2802 603 41 0 3203 0 vsize: 12976 [startup+70.0045 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3235 0 0 0 6989 9 0 0 25 0 1 0 482522525 15015936 3210 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3210 603 41 0 3625 0 vsize: 14664 [startup+80.0048 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3236 0 0 0 7988 10 0 0 25 0 1 0 482522525 15015936 3211 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3211 603 41 0 3625 0 vsize: 14664 [startup+90.0045 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 8988 10 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223728 134558839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3212 603 41 0 3625 0 vsize: 14664 [startup+100.005 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 9988 10 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3212 603 41 0 3625 0 vsize: 14664 [startup+110.005 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 10987 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3212 603 41 0 3625 0 vsize: 14664 [startup+120.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 11987 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3212 603 41 0 3625 0 vsize: 14664 [startup+130.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 12987 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3212 603 41 0 3625 0 vsize: 14664 [startup+140.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3237 0 0 0 13986 11 0 0 25 0 1 0 482522525 15015936 3212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3666 3212 603 41 0 3625 0 vsize: 14664 [startup+150.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3330 0 0 0 14986 11 0 0 25 0 1 0 482522525 15421440 3305 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3765 3305 603 41 0 3724 0 vsize: 15060 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3358 0 0 0 15986 12 0 0 25 0 1 0 482522525 15556608 3333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3798 3333 603 41 0 3757 0 vsize: 15192 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3915 0 0 0 16985 13 0 0 25 0 1 0 482522525 17842176 3890 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3890 603 41 0 4315 0 vsize: 17424 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 17985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3903 603 41 0 4315 0 vsize: 17424 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 18985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223680 134565149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3903 603 41 0 4315 0 vsize: 17424 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 19985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3903 603 41 0 4315 0 vsize: 17424 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 20985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3903 603 41 0 4315 0 vsize: 17424 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 3928 0 0 0 21985 13 0 0 25 0 1 0 482522525 17842176 3903 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3903 603 41 0 4315 0 vsize: 17424 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4187 0 0 0 22985 14 0 0 25 0 1 0 482522525 18911232 4162 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4617 4162 603 41 0 4576 0 vsize: 18468 [startup+240.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 23984 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4912 4460 603 41 0 4871 0 vsize: 19648 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 24984 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4912 4460 603 41 0 4871 0 vsize: 19648 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 25984 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223680 134565134 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4912 4460 603 41 0 4871 0 vsize: 19648 [startup+270.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4485 0 0 0 26985 15 0 0 25 0 1 0 482522525 20119552 4460 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4912 4460 603 41 0 4871 0 vsize: 19648 [startup+280.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 4700 0 0 0 27984 16 0 0 25 0 1 0 482522525 21065728 4675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5143 4675 603 41 0 5102 0 vsize: 20572 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5087 0 0 0 28983 17 0 0 25 0 1 0 482522525 22589440 5062 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5062 603 41 0 5474 0 vsize: 22060 [startup+300.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 29983 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 30983 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+320.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 31983 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+330.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 32984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 33984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+350.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 34984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 35984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 36984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+380.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 37984 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+390.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 38985 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+400.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5088 0 0 0 39985 17 0 0 25 0 1 0 482522525 22589440 5063 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5063 603 41 0 5474 0 vsize: 22060 [startup+410.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 40985 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5064 603 41 0 5474 0 vsize: 22060 [startup+420.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 41985 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5064 603 41 0 5474 0 vsize: 22060 [startup+430.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 42985 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5064 603 41 0 5474 0 vsize: 22060 [startup+440.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 43986 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5064 603 41 0 5474 0 vsize: 22060 [startup+450.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 44986 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5064 603 41 0 5474 0 vsize: 22060 [startup+460.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5089 0 0 0 45986 17 0 0 25 0 1 0 482522525 22589440 5064 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5515 5064 603 41 0 5474 0 vsize: 22060 [startup+470.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5164 0 0 0 46986 18 0 0 25 0 1 0 482522525 22994944 5139 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5614 5139 603 41 0 5573 0 vsize: 22456 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5289 0 0 0 47986 18 0 0 25 0 1 0 482522525 23400448 5264 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5713 5264 603 41 0 5672 0 vsize: 22852 [startup+490.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5308 0 0 0 48986 18 0 0 25 0 1 0 482522525 23547904 5283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5749 5283 603 41 0 5708 0 vsize: 22996 [startup+500.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5320 0 0 0 49986 18 0 0 25 0 1 0 482522525 23547904 5295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5749 5295 603 41 0 5708 0 vsize: 22996 [startup+510.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5326 0 0 0 50986 18 0 0 25 0 1 0 482522525 23687168 5301 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5301 603 41 0 5742 0 vsize: 23132 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 51986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5310 603 41 0 5742 0 vsize: 23132 [startup+530.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 52986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5310 603 41 0 5742 0 vsize: 23132 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 53986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5310 603 41 0 5742 0 vsize: 23132 [startup+550.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 54986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5310 603 41 0 5742 0 vsize: 23132 [startup+560.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5335 0 0 0 55986 18 0 0 25 0 1 0 482522525 23687168 5310 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5310 603 41 0 5742 0 vsize: 23132 [startup+570.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5341 0 0 0 56986 18 0 0 25 0 1 0 482522525 23687168 5316 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5316 603 41 0 5742 0 vsize: 23132 [startup+580.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5343 0 0 0 57987 18 0 0 25 0 1 0 482522525 23687168 5318 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5318 603 41 0 5742 0 vsize: 23132 [startup+590.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5343 0 0 0 58987 18 0 0 25 0 1 0 482522525 23687168 5318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5318 603 41 0 5742 0 vsize: 23132 [startup+600.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5344 0 0 0 59986 19 0 0 25 0 1 0 482522525 23687168 5319 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5783 5319 603 41 0 5742 0 vsize: 23132 [startup+610.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5370 0 0 0 60986 19 0 0 25 0 1 0 482522525 23834624 5345 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5819 5345 603 41 0 5778 0 vsize: 23276 [startup+620.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5391 0 0 0 61987 19 0 0 25 0 1 0 482522525 24031232 5366 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5366 603 41 0 5826 0 vsize: 23468 [startup+630.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5391 0 0 0 62987 19 0 0 25 0 1 0 482522525 24031232 5366 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5366 603 41 0 5826 0 vsize: 23468 [startup+640.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 63987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5367 603 41 0 5826 0 vsize: 23468 [startup+650.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 64987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5367 603 41 0 5826 0 vsize: 23468 [startup+660.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 65987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5367 603 41 0 5826 0 vsize: 23468 [startup+670.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5392 0 0 0 66987 19 0 0 25 0 1 0 482522525 24031232 5367 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5367 603 41 0 5826 0 vsize: 23468 [startup+680.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5414 0 0 0 67988 19 0 0 25 0 1 0 482522525 24031232 5389 4294967295 134512640 134672761 3221224544 3221223728 134558775 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5389 603 41 0 5826 0 vsize: 23468 [startup+690.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5416 0 0 0 68988 19 0 0 25 0 1 0 482522525 24031232 5391 4294967295 134512640 134672761 3221224544 3221223728 134559540 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5391 603 41 0 5826 0 vsize: 23468 [startup+700.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5416 0 0 0 69988 19 0 0 25 0 1 0 482522525 24031232 5391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5867 5391 603 41 0 5826 0 vsize: 23468 [startup+710.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5425 0 0 0 70988 19 0 0 25 0 1 0 482522525 24227840 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5400 603 41 0 5874 0 vsize: 23660 [startup+720.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5425 0 0 0 71988 19 0 0 25 0 1 0 482522525 24227840 5400 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5400 603 41 0 5874 0 vsize: 23660 [startup+730.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5425 0 0 0 72989 19 0 0 25 0 1 0 482522525 24227840 5400 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5400 603 41 0 5874 0 vsize: 23660 [startup+740.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5426 0 0 0 73989 19 0 0 25 0 1 0 482522525 24227840 5401 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5401 603 41 0 5874 0 vsize: 23660 [startup+750.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5440 0 0 0 74989 19 0 0 25 0 1 0 482522525 24227840 5415 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5415 603 41 0 5874 0 vsize: 23660 [startup+760.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5440 0 0 0 75989 19 0 0 25 0 1 0 482522525 24227840 5415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5415 603 41 0 5874 0 vsize: 23660 [startup+770.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5445 0 0 0 76989 19 0 0 25 0 1 0 482522525 24227840 5420 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5915 5420 603 41 0 5874 0 vsize: 23660 [startup+780.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5460 0 0 0 77989 19 0 0 25 0 1 0 482522525 24375296 5435 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5951 5435 603 41 0 5910 0 vsize: 23804 [startup+790.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5460 0 0 0 78990 19 0 0 25 0 1 0 482522525 24375296 5435 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5951 5435 603 41 0 5910 0 vsize: 23804 [startup+800.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5461 0 0 0 79990 19 0 0 25 0 1 0 482522525 24375296 5436 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5951 5436 603 41 0 5910 0 vsize: 23804 [startup+810.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5461 0 0 0 80990 19 0 0 25 0 1 0 482522525 24375296 5436 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5951 5436 603 41 0 5910 0 vsize: 23804 [startup+820.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5461 0 0 0 81990 19 0 0 25 0 1 0 482522525 24375296 5436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5951 5436 603 41 0 5910 0 vsize: 23804 [startup+830.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5483 0 0 0 82990 19 0 0 25 0 1 0 482522525 24375296 5458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5951 5458 603 41 0 5910 0 vsize: 23804 [startup+840.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 83991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5499 603 41 0 5990 0 vsize: 24124 [startup+850.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 84991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5499 603 41 0 5990 0 vsize: 24124 [startup+860.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 85991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5499 603 41 0 5990 0 vsize: 24124 [startup+870.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5524 0 0 0 86991 19 0 0 25 0 1 0 482522525 24702976 5499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5499 603 41 0 5990 0 vsize: 24124 [startup+880.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5525 0 0 0 87992 19 0 0 25 0 1 0 482522525 24702976 5500 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5500 603 41 0 5990 0 vsize: 24124 [startup+890.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 88992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5518 603 41 0 5990 0 vsize: 24124 [startup+900.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 89992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5518 603 41 0 5990 0 vsize: 24124 [startup+910.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 90992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5518 603 41 0 5990 0 vsize: 24124 [startup+920.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 91992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5518 603 41 0 5990 0 vsize: 24124 [startup+930.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 92992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5518 603 41 0 5990 0 vsize: 24124 [startup+940.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5543 0 0 0 93992 19 0 0 25 0 1 0 482522525 24702976 5518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6031 5518 603 41 0 5990 0 vsize: 24124 [startup+950.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5554 0 0 0 94993 19 0 0 25 0 1 0 482522525 24899584 5529 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5529 603 41 0 6038 0 vsize: 24316 [startup+960.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5569 0 0 0 95993 19 0 0 25 0 1 0 482522525 24899584 5544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5544 603 41 0 6038 0 vsize: 24316 [startup+970.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5575 0 0 0 96993 20 0 0 25 0 1 0 482522525 24899584 5550 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5550 603 41 0 6038 0 vsize: 24316 [startup+980.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5590 0 0 0 97993 20 0 0 25 0 1 0 482522525 24899584 5565 4294967295 134512640 134672761 3221224544 3221223712 134561136 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5565 603 41 0 6038 0 vsize: 24316 [startup+990.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5591 0 0 0 98993 20 0 0 25 0 1 0 482522525 24899584 5566 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5566 603 41 0 6038 0 vsize: 24316 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5591 0 0 0 99993 20 0 0 25 0 1 0 482522525 24899584 5566 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5566 603 41 0 6038 0 vsize: 24316 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 100993 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5567 603 41 0 6038 0 vsize: 24316 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 101995 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5567 603 41 0 6038 0 vsize: 24316 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 102996 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5567 603 41 0 6038 0 vsize: 24316 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 103996 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5567 603 41 0 6038 0 vsize: 24316 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5592 0 0 0 104996 20 0 0 25 0 1 0 482522525 24899584 5567 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6079 5567 603 41 0 6038 0 vsize: 24316 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5602 0 0 0 105996 20 0 0 25 0 1 0 482522525 25096192 5577 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6127 5577 603 41 0 6086 0 vsize: 24508 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5609 0 0 0 106996 20 0 0 25 0 1 0 482522525 25096192 5584 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6127 5584 603 41 0 6086 0 vsize: 24508 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5628 0 0 0 107996 20 0 0 25 0 1 0 482522525 25096192 5603 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6127 5603 603 41 0 6086 0 vsize: 24508 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5647 0 0 0 108996 20 0 0 25 0 1 0 482522525 25292800 5622 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5622 603 41 0 6134 0 vsize: 24700 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5667 0 0 0 109996 20 0 0 25 0 1 0 482522525 25292800 5642 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5642 603 41 0 6134 0 vsize: 24700 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5667 0 0 0 110997 20 0 0 25 0 1 0 482522525 25292800 5642 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5642 603 41 0 6134 0 vsize: 24700 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5671 0 0 0 111997 20 0 0 25 0 1 0 482522525 25292800 5646 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5646 603 41 0 6134 0 vsize: 24700 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5671 0 0 0 112997 20 0 0 25 0 1 0 482522525 25292800 5646 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5646 603 41 0 6134 0 vsize: 24700 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 113997 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5647 603 41 0 6134 0 vsize: 24700 [startup+1150.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 114997 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5647 603 41 0 6134 0 vsize: 24700 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 115998 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5647 603 41 0 6134 0 vsize: 24700 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5672 0 0 0 116998 20 0 0 25 0 1 0 482522525 25292800 5647 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6175 5647 603 41 0 6134 0 vsize: 24700 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5683 0 0 0 117998 20 0 0 25 0 1 0 482522525 25456640 5658 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6215 5658 603 41 0 6174 0 vsize: 24860 [startup+1190.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5710 0 0 0 118997 21 0 0 25 0 1 0 482522525 25620480 5685 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6255 5685 603 41 0 6214 0 vsize: 25020 [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12941 Raw data (stat): 12941 (minisat+) R 12940 24215 24214 0 -1 0 5734 0 0 0 119998 21 0 0 25 0 1 0 482522525 25620480 5709 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6255 5709 603 41 0 6214 0 vsize: 25020 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 12941 Raw data (stat): 12941 (minisat+) Z 12940 24215 24214 0 -1 12 5737 0 0 0 119998 22 0 0 25 0 1 0 482522525 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.06 CPU time (s): 1200.21 CPU user time (s): 1199.98 CPU system time (s): 0.222966 CPU usage (%): 100.012 Max. virtual memory (Kb): 25020 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####