Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb |
MD5SUM | e6bff154156b54af3a9a38f7579209b6 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 17324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 163 |
Biggest coefficient in the objective function | 1024 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 74742 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 8192 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 74742 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.06984 |
Number of variables | 163 |
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 | 102 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc17 THE 2005-04-20 21:03:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14715 boxname=wulflinc17 idbench=1132 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e6bff154156b54af3a9a38f7579209b6 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-neos5.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-neos5.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-neos5.opb IDLAUNCH: 14715 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 770484 kB Buffers: 33072 kB Cached: 198216 kB SwapCached: 48 kB Active: 38436 kB Inactive: 195880 kB HighTotal: 131008 kB HighFree: 8736 kB LowTotal: 903652 kB LowFree: 761748 kB SwapTotal: 2097892 kB SwapFree: 2097840 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7032 kB Slab: 23996 kB Committed_AS: 63808 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 21:23:19 (client local time) WITH STATUS 10 IN 1200.48 SECONDS stats: 14715 7 1200.48 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: 10 c ---[ 71]---> BDD-cost: 10 c ---[ 70]---> BDD-cost: 10 c ---[ 69]---> BDD-cost: 10 c ---[ 68]---> BDD-cost: 10 c ---[ 67]---> BDD-cost: 10 c ---[ 66]---> BDD-cost: 10 c ---[ 65]---> BDD-cost: 10 c ---[ 64]---> BDD-cost: 10 c ---[ 63]---> BDD-cost: 10 c ---[ 62]---> BDD-cost: 199 c ---[ 61]---> BDD-cost: 363 c ---[ 60]---> BDD-cost: 147 c ---[ 59]---> BDD-cost: 768 c ---[ 58]---> BDD-cost: 468 c ---[ 57]---> BDD-cost: 147 c ---[ 56]---> BDD-cost: 608 c ---[ 55]---> BDD-cost: 468 c ---[ 54]---> BDD-cost: 468 c ---[ 53]---> BDD-cost: 147 c ---[ 52]---> BDD-cost: 608 c ---[ 51]---> BDD-cost: 100 c ---[ 50]---> BDD-cost: 468 c ---[ 49]---> BDD-cost: 606 c ---[ 48]---> BDD-cost: 250 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: 581 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: 581 c ---[ 31]---> BDD-cost: 177 c ---[ 30]---> BDD-cost: 129 c ---[ 29]---> BDD-cost: 173 c ---[ 28]---> BDD-cost: 444 c ---[ 27]---> BDD-cost: 581 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: 418 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 | 38216 113117 | 12738 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 29697[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3374 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 44970 128900 | 14990 0 0 nan | 0.000 % | c | 100 | 44970 128900 | 16489 100 596 6.0 | 0.428 % | c | 251 | 44970 128900 | 18137 251 1549 6.2 | 0.428 % | c ============================================================================== c [1mFound solution: 21963[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 450 | 45047 129099 | 15015 450 2812 6.2 | 0.428 % | c | 550 | 45047 129099 | 16516 550 4172 7.6 | 0.433 % | c | 700 | 45047 129099 | 18168 700 5822 8.3 | 0.433 % | c | 925 | 45047 129099 | 19984 925 8796 9.5 | 0.433 % | c ============================================================================== c [1mFound solution: 20219[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 979 | 45072 129163 | 15024 979 9148 9.3 | 0.433 % | c | 1082 | 45072 129163 | 16526 1082 10773 10.0 | 0.438 % | c | 1232 | 45072 129163 | 18179 1232 11901 9.7 | 0.438 % | c | 1457 | 45072 129163 | 19996 1457 13547 9.3 | 0.438 % | c | 1795 | 45072 129163 | 21996 1795 24684 13.8 | 0.438 % | c | 2303 | 45072 129163 | 24196 2303 31039 13.5 | 0.438 % | c | 3063 | 45072 129163 | 26615 3063 48131 15.7 | 0.438 % | c | 4202 | 45072 129163 | 29277 4202 71867 17.1 | 0.438 % | c ============================================================================== c [1mFound solution: 19943[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5451 | 45080 129188 | 15026 5451 86358 15.8 | 0.438 % | c | 5551 | 45080 129188 | 16528 5551 87646 15.8 | 0.444 % | c | 5704 | 45080 129188 | 18181 5704 89470 15.7 | 0.444 % | c | 5929 | 45080 129188 | 19999 5929 94156 15.9 | 0.444 % | c | 6267 | 45080 129188 | 21999 6267 97789 15.6 | 0.444 % | c | 6773 | 45080 129188 | 24199 6773 104367 15.4 | 0.444 % | c ============================================================================== c [1mFound solution: 19942[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7273 | 45108 129262 | 15036 7273 109570 15.1 | 0.444 % | c | 7373 | 45108 129262 | 16539 7373 111221 15.1 | 0.449 % | c | 7523 | 45108 129262 | 18193 7523 112313 14.9 | 0.449 % | c | 7748 | 45108 129262 | 20012 7748 116589 15.0 | 0.449 % | c | 8085 | 45108 129262 | 22014 8085 120472 14.9 | 0.449 % | c ============================================================================== c [1mFound solution: 18550[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8459 | 45118 129289 | 15039 8459 129457 15.3 | 0.449 % | c ============================================================================== c [1mFound solution: 18329[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8512 | 45148 129369 | 15049 8512 130576 15.3 | 0.449 % | c | 8612 | 45142 129357 | 16553 8582 132027 15.4 | 0.477 % | c | 8762 | 45142 129357 | 18209 8732 134291 15.4 | 0.477 % | c | 8990 | 45142 129357 | 20030 8960 137640 15.4 | 0.477 % | c | 9328 | 45142 129357 | 22033 9298 143509 15.4 | 0.477 % | c | 9836 | 45142 129357 | 24236 9806 155537 15.9 | 0.477 % | c | 10595 | 45142 129357 | 26660 10565 172988 16.4 | 0.477 % | c | 11735 | 45142 129357 | 29326 11705 185659 15.9 | 0.477 % | c | 13444 | 45142 129357 | 32258 13414 225240 16.8 | 0.477 % | c | 16007 | 45142 129357 | 35484 15977 337754 21.1 | 0.477 % | c | 19851 | 45142 129357 | 39033 19821 429705 21.7 | 0.477 % | c ============================================================================== c [1mFound solution: 17910[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22838 | 45148 129377 | 15049 22808 493591 21.6 | 0.477 % | c | 22938 | 45148 129377 | 16553 11504 278856 24.2 | 0.483 % | c | 23089 | 45148 129377 | 18209 11655 283539 24.3 | 0.483 % | c | 23314 | 45148 129377 | 20030 11880 289063 24.3 | 0.483 % | c | 23651 | 45148 129377 | 22033 12217 296504 24.3 | 0.483 % | c | 24158 | 45148 129377 | 24236 12724 312622 24.6 | 0.483 % | c | 24917 | 45148 129377 | 26660 13483 336779 25.0 | 0.483 % | c | 26058 | 45148 129377 | 29326 14624 360791 24.7 | 0.483 % | c | 27766 | 45148 129377 | 32258 16332 390294 23.9 | 0.483 % | c ============================================================================== c [1mFound solution: 17908[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28097 | 45156 129405 | 15052 16663 395852 23.8 | 0.483 % | c | 28198 | 45156 129405 | 16557 8433 163786 19.4 | 0.489 % | c | 28349 | 45156 129405 | 18212 8584 166466 19.4 | 0.489 % | c | 28575 | 45156 129405 | 20034 8810 174167 19.8 | 0.489 % | c | 28913 | 45156 129405 | 22037 9148 180336 19.7 | 0.489 % | c | 29419 | 45156 129405 | 24241 9654 193330 20.0 | 0.489 % | c | 30178 | 45154 129401 | 26665 10410 227671 21.9 | 0.494 % | c | 31318 | 45154 129401 | 29332 11550 256723 22.2 | 0.494 % | c | 33027 | 45154 129401 | 32265 13259 304794 23.0 | 0.494 % | c | 35589 | 45154 129401 | 35491 15821 369487 23.4 | 0.494 % | c | 39433 | 45154 129401 | 39041 19665 470920 23.9 | 0.494 % | c ============================================================================== c [1mFound solution: 17907[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44851 | 45156 129411 | 15052 21563 494051 22.9 | 0.494 % | c | 44951 | 45156 129411 | 16557 10806 191548 17.7 | 0.511 % | c | 45101 | 45156 129411 | 18212 10956 194077 17.7 | 0.511 % | c | 45326 | 45156 129411 | 20034 11181 197764 17.7 | 0.511 % | c | 45664 | 45156 129411 | 22037 11519 207314 18.0 | 0.511 % | c | 46170 | 45156 129411 | 24241 12025 216411 18.0 | 0.511 % | c | 46931 | 45156 129411 | 26665 12786 230651 18.0 | 0.511 % | c ============================================================================== c [1mFound solution: 17906[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47662 | 45164 129435 | 15054 13517 240957 17.8 | 0.511 % | c | 47762 | 45164 129435 | 16559 13617 243021 17.8 | 0.517 % | c | 47914 | 45164 129435 | 18215 13769 247263 18.0 | 0.517 % | c | 48140 | 45164 129435 | 20036 13995 252411 18.0 | 0.517 % | c | 48477 | 45164 129435 | 22040 14332 255755 17.8 | 0.517 % | c | 48984 | 45164 129435 | 24244 14839 266946 18.0 | 0.517 % | c | 49744 | 45164 129435 | 26669 15599 276261 17.7 | 0.517 % | c | 50883 | 45164 129435 | 29335 16738 302685 18.1 | 0.517 % | c | 52592 | 45164 129435 | 32269 18447 323906 17.6 | 0.517 % | c ============================================================================== c [1mFound solution: 17881[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54227 | 45164 129438 | 15054 20070 346105 17.2 | 0.517 % | c | 54328 | 45164 129438 | 16559 10136 133874 13.2 | 0.540 % | c | 54480 | 45164 129438 | 18215 10288 135748 13.2 | 0.540 % | c | 54707 | 45164 129438 | 20036 10515 139720 13.3 | 0.540 % | c | 55045 | 45164 129438 | 22040 10853 145470 13.4 | 0.540 % | c | 55551 | 45164 129438 | 24244 11359 157053 13.8 | 0.540 % | c | 56310 | 45164 129438 | 26669 12118 172998 14.3 | 0.540 % | c | 57451 | 45164 129438 | 29335 13259 217181 16.4 | 0.540 % | c | 59159 | 45161 129431 | 32269 14735 235735 16.0 | 0.551 % | c | 61721 | 45161 129431 | 35496 17297 289577 16.7 | 0.551 % | c | 65566 | 45161 129431 | 39046 21142 451859 21.4 | 0.551 % | c | 71332 | 45161 129431 | 42950 26908 626497 23.3 | 0.551 % | c ============================================================================== c [1mFound solution: 17744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 73974 | 45174 129462 | 15058 29550 656185 22.2 | 0.551 % | c | 74074 | 45174 129462 | 16563 14875 330355 22.2 | 0.557 % | c ============================================================================== c [1mFound solution: 17708[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 74180 | 45186 129491 | 15062 14981 332367 22.2 | 0.557 % | c | 74281 | 45186 129491 | 16568 15082 333790 22.1 | 0.562 % | c | 74431 | 45186 129491 | 18225 15232 337872 22.2 | 0.562 % | c | 74657 | 45186 129491 | 20047 15458 342958 22.2 | 0.562 % | c | 74995 | 45186 129491 | 22052 15796 351839 22.3 | 0.562 % | c | 75503 | 45186 129491 | 24257 16304 374147 22.9 | 0.562 % | c | 76262 | 45186 129491 | 26683 17063 403068 23.6 | 0.562 % | c | 77403 | 45186 129491 | 29351 18204 448840 24.7 | 0.562 % | c | 79111 | 45186 129491 | 32286 19912 527956 26.5 | 0.562 % | c | 81673 | 45186 129491 | 35515 22474 603312 26.8 | 0.562 % | c | 85517 | 45186 129491 | 39066 26318 719234 27.3 | 0.562 % | c | 91283 | 45186 129491 | 42973 32084 873913 27.2 | 0.562 % | c ============================================================================== c [1mFound solution: 17707[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94080 | 45195 129512 | 15065 34881 917537 26.3 | 0.562 % | c | 94180 | 45195 129512 | 16571 8100 107641 13.3 | 0.568 % | c | 94330 | 45195 129512 | 18228 8250 110659 13.4 | 0.568 % | c | 94555 | 45195 129512 | 20051 8475 113822 13.4 | 0.568 % | c | 94893 | 45195 129512 | 22056 8813 119387 13.5 | 0.568 % | c ============================================================================== c [1mFound solution: 17705[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 95339 | 45206 129538 | 15068 9259 126252 13.6 | 0.568 % | c | 95439 | 45206 129538 | 16574 9359 127798 13.7 | 0.574 % | c | 95590 | 45206 129538 | 18232 9510 129902 13.7 | 0.574 % | c | 95816 | 45206 129538 | 20055 9736 132417 13.6 | 0.573 % | c | 96154 | 45206 129538 | 22061 10074 138763 13.8 | 0.574 % | c ============================================================================== c [1mFound solution: 17704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 96397 | 45217 129564 | 15072 10317 141901 13.8 | 0.574 % | c | 96497 | 45217 129564 | 16579 10417 143886 13.8 | 0.579 % | c | 96648 | 45217 129564 | 18237 10568 146385 13.9 | 0.579 % | c | 96873 | 45217 129564 | 20060 10793 148416 13.8 | 0.579 % | c | 97211 | 45217 129564 | 22066 11131 156231 14.0 | 0.579 % | c | 97718 | 45217 129564 | 24273 11638 165552 14.2 | 0.579 % | c | 98478 | 45217 129564 | 26700 12398 197214 15.9 | 0.579 % | c | 99618 | 45217 129564 | 29371 13538 214443 15.8 | 0.579 % | c | 101326 | 45217 129564 | 32308 15246 241163 15.8 | 0.579 % | c | 103888 | 45217 129564 | 35538 17808 293941 16.5 | 0.579 % | c | 107732 | 45217 129564 | 39092 21652 452320 20.9 | 0.579 % | c ============================================================================== c [1mFound solution: 17670[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 108763 | 45226 129584 | 15075 22683 470067 20.7 | 0.579 % | c | 108863 | 45226 129584 | 16582 11442 249439 21.8 | 0.585 % | c | 109014 | 45226 129584 | 18240 11593 251875 21.7 | 0.585 % | c | 109239 | 45226 129584 | 20064 11818 258172 21.8 | 0.585 % | c | 109576 | 45226 129584 | 22071 12155 264006 21.7 | 0.585 % | c | 110082 | 45226 129584 | 24278 12661 272113 21.5 | 0.585 % | c | 110841 | 45226 129584 | 26706 13420 301628 22.5 | 0.585 % | c | 111981 | 45226 129584 | 29376 14560 353324 24.3 | 0.585 % | c ============================================================================== c [1mFound solution: 17666[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 113497 | 45237 129609 | 15079 16076 376343 23.4 | 0.585 % | c | 113597 | 45235 129605 | 16586 8137 142448 17.5 | 0.596 % | c | 113747 | 45235 129605 | 18245 8287 145023 17.5 | 0.596 % | c | 113972 | 45235 129605 | 20070 8512 148477 17.4 | 0.596 % | c | 114309 | 45235 129605 | 22077 8849 154191 17.4 | 0.596 % | c | 114818 | 45235 129605 | 24284 9358 175848 18.8 | 0.596 % | c | 115579 | 45235 129605 | 26713 10119 188714 18.6 | 0.596 % | c | 116718 | 45235 129605 | 29384 11258 216825 19.3 | 0.596 % | c | 118428 | 45235 129605 | 32323 12968 239716 18.5 | 0.596 % | c | 120991 | 45235 129605 | 35555 15531 280360 18.1 | 0.596 % | c | 124835 | 45235 129605 | 39111 19375 355471 18.3 | 0.596 % | c | 130601 | 45235 129605 | 43022 25141 522403 20.8 | 0.596 % | c | 139250 | 45235 129605 | 47324 33790 721872 21.4 | 0.596 % | c ============================================================================== c [1mFound solution: 17665[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 139503 | 45245 129627 | 15081 34043 725424 21.3 | 0.596 % | c | 139603 | 45245 129627 | 16589 8341 109622 13.1 | 0.602 % | c | 139753 | 45245 129627 | 18248 8491 111234 13.1 | 0.602 % | c | 139978 | 45245 129627 | 20072 8716 114482 13.1 | 0.602 % | c | 140315 | 45245 129627 | 22080 9053 121179 13.4 | 0.602 % | c ============================================================================== c [1mFound solution: 17664[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 140528 | 45256 129652 | 15085 9266 124871 13.5 | 0.602 % | c | 140628 | 45256 129652 | 16593 9366 127928 13.7 | 0.607 % | c | 140778 | 45256 129652 | 18252 9516 129663 13.6 | 0.607 % | c | 141003 | 45256 129652 | 20078 9741 134269 13.8 | 0.607 % | c | 141341 | 45256 129652 | 22085 10079 138173 13.7 | 0.607 % | c | 141848 | 45256 129652 | 24294 10586 156334 14.8 | 0.607 % | c | 142607 | 45256 129652 | 26723 11345 173302 15.3 | 0.607 % | c ============================================================================== c [1mFound solution: 17591[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 143326 | 45262 129666 | 15087 12064 193899 16.1 | 0.607 % | c | 143426 | 45262 129666 | 16595 12164 196104 16.1 | 0.613 % | c | 143577 | 45262 129666 | 18255 12315 199946 16.2 | 0.613 % | c | 143804 | 45262 129666 | 20080 12542 203900 16.3 | 0.613 % | c | 144141 | 45262 129666 | 22088 12879 213936 16.6 | 0.613 % | c | 144647 | 45262 129666 | 24297 13385 221679 16.6 | 0.613 % | c | 145407 | 45262 129666 | 26727 14145 249299 17.6 | 0.613 % | c | 146548 | 45262 129666 | 29400 15286 273392 17.9 | 0.613 % | c | 148256 | 45262 129666 | 32340 16994 307763 18.1 | 0.613 % | c ============================================================================== c [1mFound solution: 17590[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 149001 | 45271 129688 | 15090 17739 320641 18.1 | 0.613 % | c | 149101 | 45271 129688 | 16599 8970 135776 15.1 | 0.618 % | c | 149252 | 45271 129688 | 18258 9121 138552 15.2 | 0.618 % | c | 149477 | 45271 129688 | 20084 9346 141060 15.1 | 0.618 % | c | 149814 | 45271 129688 | 22093 9683 148185 15.3 | 0.618 % | c | 150320 | 45271 129688 | 24302 10189 155152 15.2 | 0.618 % | c | 151079 | 45271 129688 | 26732 10948 178788 16.3 | 0.618 % | c | 152218 | 45271 129688 | 29406 12087 198860 16.5 | 0.618 % | c ============================================================================== c [1mFound solution: 17586[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 153213 | 45280 129710 | 15093 13082 214979 16.4 | 0.618 % | c | 153313 | 45280 129710 | 16602 13182 217732 16.5 | 0.624 % | c | 153463 | 45280 129710 | 18262 13332 220002 16.5 | 0.624 % | c | 153689 | 45280 129710 | 20088 13558 226210 16.7 | 0.624 % | c | 154027 | 45280 129710 | 22097 13896 235837 17.0 | 0.624 % | c ============================================================================== c [1mFound solution: 17585[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 154341 | 45289 129732 | 15096 14210 241346 17.0 | 0.624 % | c | 154441 | 45289 129732 | 16605 14310 244266 17.1 | 0.629 % | c | 154591 | 45289 129732 | 18266 14460 247696 17.1 | 0.629 % | c | 154816 | 45289 129732 | 20092 14685 251985 17.2 | 0.629 % | c | 155153 | 45287 129728 | 22102 15021 254936 17.0 | 0.635 % | c | 155659 | 45287 129728 | 24312 15527 264999 17.1 | 0.635 % | c | 156419 | 45287 129728 | 26743 16287 275773 16.9 | 0.635 % | c | 157558 | 45287 129728 | 29417 17426 288256 16.5 | 0.635 % | c | 159266 | 45287 129728 | 32359 19134 331560 17.3 | 0.635 % | c | 161828 | 45287 129728 | 35595 21696 407434 18.8 | 0.635 % | c ============================================================================== c [1mFound solution: 17584[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 163924 | 45296 129749 | 15098 23792 454862 19.1 | 0.635 % | c | 164025 | 45296 129749 | 16607 11997 198621 16.6 | 0.641 % | c | 164176 | 45296 129749 | 18268 12148 202316 16.7 | 0.641 % | c | 164401 | 45296 129749 | 20095 12373 205680 16.6 | 0.641 % | c | 164738 | 45296 129749 | 22104 12710 212026 16.7 | 0.641 % | c | 165246 | 45296 129749 | 24315 13218 230408 17.4 | 0.641 % | c | 166006 | 45296 129749 | 26747 13978 249559 17.9 | 0.641 % | c ============================================================================== c [1mFound solution: 17526[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 166765 | 45303 129764 | 15101 14737 265748 18.0 | 0.641 % | c | 166866 | 45303 129764 | 16611 14838 268020 18.1 | 0.646 % | c | 167016 | 45303 129764 | 18272 14988 270599 18.1 | 0.646 % | c | 167241 | 45303 129764 | 20099 15213 273825 18.0 | 0.646 % | c | 167578 | 45303 129764 | 22109 15550 281856 18.1 | 0.646 % | c ============================================================================== c [1mFound solution: 17525[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 167931 | 45310 129784 | 15103 15903 287964 18.1 | 0.646 % | c | 168031 | 45310 129784 | 16613 8052 104714 13.0 | 0.652 % | c | 168181 | 45310 129784 | 18274 8202 105679 12.9 | 0.652 % | c | 168409 | 45310 129784 | 20102 8430 108145 12.8 | 0.652 % | c | 168750 | 45310 129784 | 22112 8771 115494 13.2 | 0.652 % | c | 169258 | 45310 129784 | 24323 9279 130507 14.1 | 0.652 % | c | 170017 | 45310 129784 | 26755 10038 149123 14.9 | 0.652 % | c | 171156 | 45310 129784 | 29431 11177 163357 14.6 | 0.652 % | c | 172864 | 45310 129784 | 32374 12885 210231 16.3 | 0.652 % | c ============================================================================== c [1mFound solution: 17494[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 173207 | 45320 129807 | 15106 13228 214195 16.2 | 0.652 % | c | 173308 | 45320 129807 | 16616 13329 216012 16.2 | 0.657 % | c | 173458 | 45320 129807 | 18278 13479 217357 16.1 | 0.657 % | c | 173683 | 45318 129803 | 20106 13701 219583 16.0 | 0.663 % | c | 174020 | 45318 129803 | 22116 14038 225445 16.1 | 0.663 % | c | 174526 | 45318 129803 | 24328 14544 230665 15.9 | 0.663 % | c ============================================================================== c [1mFound solution: 17446[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 175063 | 45326 129821 | 15108 15081 239249 15.9 | 0.663 % | c | 175163 | 45326 129821 | 16618 15181 240968 15.9 | 0.669 % | c | 175314 | 45326 129821 | 18280 15332 243534 15.9 | 0.669 % | c | 175539 | 45326 129821 | 20108 15557 248220 16.0 | 0.669 % | c | 175876 | 45326 129821 | 22119 15894 256913 16.2 | 0.669 % | c | 176382 | 45326 129821 | 24331 16400 264900 16.2 | 0.669 % | c | 177141 | 45326 129821 | 26764 17159 286459 16.7 | 0.669 % | c ============================================================================== c [1mFound solution: 17445[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 177433 | 45337 129847 | 15112 17451 290547 16.6 | 0.669 % | c | 177533 | 45337 129847 | 16623 8826 95481 10.8 | 0.674 % | c | 177683 | 45337 129847 | 18285 8976 98347 11.0 | 0.674 % | c | 177908 | 45337 129847 | 20114 9201 101894 11.1 | 0.674 % | c | 178245 | 45337 129847 | 22125 9538 107326 11.3 | 0.674 % | c | 178752 | 45337 129847 | 24338 10045 116787 11.6 | 0.674 % | c ============================================================================== c [1mFound solution: 17430[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 179088 | 45344 129862 | 15114 10381 122242 11.8 | 0.674 % | c | 179188 | 45344 129862 | 16625 10481 126796 12.1 | 0.680 % | c | 179338 | 45344 129862 | 18287 10631 131016 12.3 | 0.680 % | c ============================================================================== c [1mFound solution: 17429[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 179541 | 45353 129882 | 15117 10834 132998 12.3 | 0.680 % | c | 179641 | 45353 129882 | 16628 10934 134549 12.3 | 0.685 % | c | 179791 | 45353 129882 | 18291 11084 137114 12.4 | 0.685 % | c | 180016 | 45353 129882 | 20120 11309 142304 12.6 | 0.685 % | c | 180354 | 45353 129882 | 22132 11647 149217 12.8 | 0.685 % | c | 180860 | 45353 129882 | 24346 12153 159113 13.1 | 0.685 % | c ============================================================================== c [1mFound solution: 17428[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 181577 | 45362 129903 | 15120 12870 179956 14.0 | 0.685 % | c | 181677 | 45362 129903 | 16632 12970 182391 14.1 | 0.691 % | c | 181827 | 45362 129903 | 18295 13120 185776 14.2 | 0.691 % | c | 182053 | 45362 129903 | 20124 13346 191843 14.4 | 0.691 % | c | 182390 | 45362 129903 | 22137 13683 201566 14.7 | 0.691 % | c | 182897 | 45362 129903 | 24350 14190 216587 15.3 | 0.691 % | c | 183656 | 45362 129903 | 26786 14949 233329 15.6 | 0.691 % | c | 184795 | 45362 129903 | 29464 16088 264289 16.4 | 0.691 % | c | 186503 | 45362 129903 | 32411 17796 315662 17.7 | 0.691 % | c ============================================================================== c [1mFound solution: 17427[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 186822 | 45371 129924 | 15123 18115 321510 17.7 | 0.691 % | c | 186922 | 45371 129924 | 16635 9158 136413 14.9 | 0.697 % | c | 187072 | 45371 129924 | 18298 9308 138870 14.9 | 0.697 % | c | 187298 | 45371 129924 | 20128 9534 145509 15.3 | 0.697 % | c | 187635 | 45371 129924 | 22141 9871 154695 15.7 | 0.697 % | c | 188142 | 45371 129924 | 24355 10378 169704 16.4 | 0.697 % | c ============================================================================== c [1mFound solution: 17426[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 188256 | 45380 129944 | 15126 10492 171355 16.3 | 0.697 % | c | 188356 | 45380 129944 | 16638 10592 173408 16.4 | 0.702 % | c | 188509 | 45380 129944 | 18302 10745 176703 16.4 | 0.702 % | c | 188735 | 45380 129944 | 20132 10971 182669 16.7 | 0.702 % | c | 189072 | 45380 129944 | 22145 11308 188064 16.6 | 0.702 % | c | 189579 | 45380 129944 | 24360 11815 195762 16.6 | 0.702 % | c | 190339 | 45380 129944 | 26796 12575 209096 16.6 | 0.702 % | c | 191482 | 45380 129944 | 29476 13718 233710 17.0 | 0.702 % | c | 193190 | 45380 129944 | 32423 15426 263074 17.1 | 0.702 % | c | 195752 | 45380 129944 | 35666 17988 333864 18.6 | 0.702 % | c ============================================================================== c [1mFound solution: 17425[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 196158 | 45389 129964 | 15129 18394 340225 18.5 | 0.702 % | c | 196258 | 45389 129964 | 16641 9297 128447 13.8 | 0.708 % | c | 196408 | 45389 129964 | 18306 9447 132555 14.0 | 0.708 % | c | 196633 | 45389 129964 | 20136 9672 137237 14.2 | 0.708 % | c | 196971 | 45389 129964 | 22150 10010 145208 14.5 | 0.708 % | c | 197478 | 45389 129964 | 24365 10517 155366 14.8 | 0.708 % | c | 198237 | 45389 129964 | 26801 11276 173759 15.4 | 0.708 % | c | 199377 | 45389 129964 | 29482 12416 192821 15.5 | 0.708 % | c | 201085 | 45389 129964 | 32430 14124 226614 16.0 | 0.708 % | c | 203649 | 45389 129964 | 35673 16688 287311 17.2 | 0.708 % | c ============================================================================== c [1mFound solution: 17422[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 205292 | 45401 129991 | 15133 18331 343530 18.7 | 0.708 % | c | 205392 | 45401 129991 | 16646 9266 143788 15.5 | 0.713 % | c | 205542 | 45401 129991 | 18310 9416 145392 15.4 | 0.713 % | c | 205768 | 45401 129991 | 20142 9642 148989 15.5 | 0.713 % | c | 206105 | 45401 129991 | 22156 9979 155217 15.6 | 0.713 % | c | 206611 | 45401 129991 | 24371 10485 168291 16.1 | 0.713 % | c | 207370 | 45401 129991 | 26809 11244 182328 16.2 | 0.713 % | c ============================================================================== c [1mFound solution: 16390[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 207976 | 45409 130011 | 15136 11850 199471 16.8 | 0.713 % | c | 208077 | 45409 130011 | 16649 11951 201946 16.9 | 0.719 % | c | 208227 | 45409 130011 | 18314 12101 204961 16.9 | 0.719 % | c | 208452 | 45409 130011 | 20146 12326 209392 17.0 | 0.719 % | c | 208790 | 45409 130011 | 22160 12664 218390 17.2 | 0.719 % | c | 209297 | 45409 130011 | 24376 13171 225716 17.1 | 0.719 % | c | 210056 | 45409 130011 | 26814 13930 244150 17.5 | 0.719 % | c | 211195 | 45409 130011 | 29495 15069 276080 18.3 | 0.719 % | c | 212904 | 45409 130011 | 32445 16778 325749 19.4 | 0.719 % | c ============================================================================== c [1mFound solution: 16386[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 214943 | 45414 130022 | 15138 18817 362124 19.2 | 0.719 % | c | 215043 | 45414 130022 | 16651 9509 131383 13.8 | 0.724 % | c | 215193 | 45414 130022 | 18316 9659 135268 14.0 | 0.724 % | c | 215419 | 45414 130022 | 20148 9885 139858 14.1 | 0.724 % | c | 215756 | 45414 130022 | 22163 10222 150133 14.7 | 0.724 % | c | 216264 | 45414 130022 | 24379 10730 164196 15.3 | 0.724 % | c | 217026 | 45414 130022 | 26817 11492 180266 15.7 | 0.724 % | c | 218166 | 45414 130022 | 29499 12632 195116 15.4 | 0.724 % | c | 219874 | 45414 130022 | 32449 14340 243475 17.0 | 0.724 % | c ============================================================================== c [1mFound solution: 16385[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 221263 | 45420 130035 | 15140 15729 302709 19.2 | 0.724 % | c | 221367 | 45420 130035 | 16654 7969 132837 16.7 | 0.730 % | c | 221518 | 45420 130035 | 18319 8120 136244 16.8 | 0.730 % | c | 221745 | 45420 130035 | 20151 8347 143499 17.2 | 0.730 % | c | 222084 | 45420 130035 | 22166 8686 151348 17.4 | 0.730 % | c | 222591 | 45420 130035 | 24383 9193 164491 17.9 | 0.730 % | c | 223351 | 45420 130035 | 26821 9953 186282 18.7 | 0.730 % | c | 224490 | 45420 130035 | 29503 11092 208715 18.8 | 0.730 % | c | 226199 | 45420 130035 | 32453 12801 260651 20.4 | 0.730 % | c | 228761 | 45420 130035 | 35699 15363 321071 20.9 | 0.730 % | c | 232606 | 45420 130035 | 39269 19208 530660 27.6 | 0.730 % | c | 238372 | 45420 130035 | 43196 24974 614466 24.6 | 0.730 % | c | 247022 | 45411 130016 | 47515 33618 958943 28.5 | 0.759 % | c | 259996 | 45411 130016 | 52267 46592 1403324 30.1 | 0.759 % | c ============================================================================== c [1mFound solution: 16384[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 276964 | 45416 130027 | 15138 28788 924703 32.1 | 0.759 % | c | 277066 | 45416 130027 | 16651 14496 431943 29.8 | 0.764 % | c | 277216 | 45416 130027 | 18316 14646 434769 29.7 | 0.764 % | c | 277441 | 45416 130027 | 20148 14871 439986 29.6 | 0.764 % | c | 277779 | 45416 130027 | 22163 15209 442704 29.1 | 0.764 % | c | 278286 | 45416 130027 | 24379 15716 453389 28.8 | 0.764 % | c | 279045 | 45416 130027 | 26817 16475 465559 28.3 | 0.764 % | c | 280184 | 45416 130027 | 29499 17614 493455 28.0 | 0.764 % | c | 281892 | 45416 130027 | 32449 19322 555797 28.8 | 0.764 % | c | 284454 | 45416 130027 | 35694 21884 650442 29.7 | 0.764 % | c | 288298 | 45416 130027 | 39264 25728 850219 33.0 | 0.764 % | c | 294064 | 45416 130027 | 43190 31494 1089927 34.6 | 0.764 % | c | 302713 | 45416 130027 | 47509 40143 1450889 36.1 | 0.764 % | c | 315689 | 45416 130027 | 52260 23375 631232 27.0 | 0.764 % | c ============================================================================== c [1mFound solution: 16333[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 329262 | 45434 130073 | 15144 36948 1669939 45.2 | 0.764 % | c | 329365 | 45434 130073 | 16658 8441 468180 55.5 | 0.786 % | c | 329517 | 45434 130073 | 18324 8593 471798 54.9 | 0.786 % | c | 329743 | 45434 130073 | 20156 8819 477245 54.1 | 0.786 % | c | 330081 | 45434 130073 | 22172 9157 484368 52.9 | 0.786 % | c | 330587 | 45434 130073 | 24389 9663 496174 51.3 | 0.786 % | c | 331346 | 45434 130073 | 26828 10422 516398 49.5 | 0.786 % | c | 332485 | 45434 130073 | 29511 11561 544250 47.1 | 0.786 % | c | 334193 | 45434 130073 | 32462 13269 602950 45.4 | 0.786 % | c | 336756 | 45434 130073 | 35708 15832 678476 42.9 | 0.786 % | c | 340602 | 45434 130073 | 39279 19678 809481 41.1 | 0.786 % | c | 346368 | 45434 130073 | 43207 25444 977814 38.4 | 0.786 % | c | 355019 | 45434 130073 | 47528 34095 1346596 39.5 | 0.786 % | c | 367995 | 45434 130073 | 52281 47071 1869611 39.7 | 0.786 % | c | 387457 | 45434 130073 | 57509 32553 988593 30.4 | 0.786 % | c | 416649 | 45434 130073 | 63260 21643 507948 23.5 | 0.786 % | c ============================================================================== c [1mFound solution: 16118[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 459125 | 45442 130094 | 15147 64119 2195192 34.2 | 0.786 % | c | 459227 | 45442 130094 | 16661 9929 219902 22.1 | 0.792 % | c | 459377 | 45442 130094 | 18327 10079 224220 22.2 | 0.792 % | c | 459602 | 45442 130094 | 20160 10304 230028 22.3 | 0.792 % | c | 459939 | 45442 130094 | 22176 10641 241843 22.7 | 0.792 % | c | 460446 | 45442 130094 | 24394 11148 259194 23.3 | 0.792 % | c | 461205 | 45442 130094 | 26833 11907 280344 23.5 | 0.792 % | c | 462344 | 45442 130094 | 29517 13046 318586 24.4 | 0.792 % | c | 464053 | 45442 130094 | 32468 14755 376570 25.5 | 0.792 % | c | 466615 | 45442 130094 | 35715 17317 467468 27.0 | 0.792 % | c | 470460 | 45442 130094 | 39287 21162 616474 29.1 | 0.792 % | c | 476228 | 45442 130094 | 43216 26930 840213 31.2 | 0.792 % | c | 484879 | 45442 130094 | 47537 35581 1198988 33.7 | 0.792 % | c | 497853 | 45442 130094 | 52291 18763 578014 30.8 | 0.792 % | c | 517316 | 45442 130094 | 57520 38226 1367300 35.8 | 0.792 % | c | 546510 | 45442 130094 | 63272 29077 944571 32.5 | 0.792 % | c | 590301 | 45442 130094 | 69600 29740 936634 31.5 | 0.792 % | c | 655986 | 45442 130094 | 76560 47036 1551733 33.0 | 0.792 % | c ============================================================================== c [1mFound solution: 16115[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 695134 | 45449 130113 | 15149 25950 1109611 42.8 | 0.792 % | c | 695235 | 45449 130113 | 16663 13076 383986 29.4 | 0.797 % | c | 695387 | 45449 130113 | 18330 13228 385208 29.1 | 0.797 % | c | 695612 | 45449 130113 | 20163 13453 387240 28.8 | 0.797 % | c | 695949 | 45449 130113 | 22179 13790 390894 28.3 | 0.797 % | c | 696455 | 45449 130113 | 24397 14296 402721 28.2 | 0.797 % | c | 697214 | 45449 130113 | 26837 15055 428611 28.5 | 0.797 % | c | 698353 | 45449 130113 | 29521 16194 463269 28.6 | 0.797 % | c | 700061 | 45449 130113 | 32473 17902 511684 28.6 | 0.797 % | c | 702624 | 45449 130113 | 35720 20465 587691 28.7 | 0.797 % | c | 706468 | 45449 130113 | 39292 24309 723802 29.8 | 0.797 % | c | 712234 | 45449 130113 | 43221 30075 910355 30.3 | 0.797 % | c | 720883 | 45449 130113 | 47544 38724 1193104 30.8 | 0.797 % | c ============================================================================== c [1mFound solution: 16114[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 730427 | 45456 130131 | 15152 48268 1482551 30.7 | 0.797 % | c | 730527 | 45456 130131 | 16667 8762 115223 13.2 | 0.803 % | c | 730677 | 45456 130131 | 18333 8912 118418 13.3 | 0.803 % | c | 730903 | 45456 130131 | 20167 9138 124304 13.6 | 0.803 % | c | 731240 | 45456 130131 | 22184 9475 131690 13.9 | 0.803 % | c | 731746 | 45456 130131 | 24402 9981 145132 14.5 | 0.803 % | c | 732505 | 45456 130131 | 26842 10740 167390 15.6 | 0.803 % | c | 733644 | 45456 130131 | 29526 11879 201857 17.0 | 0.803 % | c | 735353 | 45456 130131 | 32479 13588 253888 18.7 | 0.803 % | c | 737915 | 45456 130131 | 35727 16150 333515 20.7 | 0.803 % | c | 741759 | 45456 130131 | 39300 19994 451995 22.6 | 0.803 % | c | 747526 | 45456 130131 | 43230 25761 632647 24.6 | 0.803 % | c | 756176 | 45456 130131 | 47553 34411 1045292 30.4 | 0.803 % | c | 769151 | 45456 130131 | 52308 47386 1633754 34.5 | 0.803 % | c | 788614 | 45456 130131 | 57539 32322 970970 30.0 | 0.803 % | c ============================================================================== c [1mFound solution: 16106[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 813879 | 45465 130155 | 15155 57587 2028556 35.2 | 0.803 % | c | 813979 | 45465 130155 | 16670 8829 169193 19.2 | 0.808 % | c | 814130 | 45465 130155 | 18337 8980 171065 19.0 | 0.808 % | c | 814355 | 45465 130155 | 20171 9205 175061 19.0 | 0.808 % | c | 814692 | 45465 130155 | 22188 9542 181094 19.0 | 0.808 % | c | 815200 | 45465 130155 | 24407 10050 190585 19.0 | 0.808 % | c | 815960 | 45465 130155 | 26848 10810 206527 19.1 | 0.808 % | c | 817100 | 45465 130155 | 29532 11950 226939 19.0 | 0.808 % | c | 818808 | 45465 130155 | 32486 13658 259149 19.0 | 0.808 % | c | 821370 | 45465 130155 | 35734 16220 301543 18.6 | 0.808 % | c | 825214 | 45465 130155 | 39308 20064 365377 18.2 | 0.808 % | c | 830982 | 45459 130142 | 43238 25827 515423 20.0 | 0.819 % | c | 839632 | 45459 130142 | 47562 34477 805724 23.4 | 0.819 % | c | 852606 | 45459 130142 | 52319 47451 1286882 27.1 | 0.819 % | c ============================================================================== c [1mFound solution: 16104[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 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 869468 | 45466 130160 | 15155 25565 995028 38.9 | 0.819 % | #### 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.90 0.96 0.86 2/55 15796 Raw data (stat): 15796 (runsolver) R 15795 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539537392 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.0001 s] Raw data (loadavg): 0.91 0.96 0.86 2/55 15796 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2257 0 0 0 994 5 0 0 25 0 1 0 539537392 12034048 2230 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2938 2230 603 41 0 2897 0 vsize: 11752 [startup+20.0006 s] Raw data (loadavg): 0.92 0.96 0.86 2/55 15796 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2485 0 0 0 1993 5 0 0 25 0 1 0 539537392 12906496 2458 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3151 2458 603 41 0 3110 0 vsize: 12604 [startup+30.0012 s] Raw data (loadavg): 0.94 0.96 0.87 2/55 15796 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2604 0 0 0 2992 5 0 0 25 0 1 0 539537392 13447168 2577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3283 2577 603 41 0 3242 0 vsize: 13132 [startup+40.0009 s] Raw data (loadavg): 0.94 0.96 0.87 2/55 15796 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2632 0 0 0 3992 6 0 0 25 0 1 0 539537392 13578240 2605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3315 2605 603 41 0 3274 0 vsize: 13260 [startup+50.0001 s] Raw data (loadavg): 0.95 0.96 0.87 2/55 15796 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2705 0 0 0 4992 6 0 0 25 0 1 0 539537392 13848576 2678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3381 2678 603 41 0 3340 0 vsize: 13524 [startup+60.0004 s] Raw data (loadavg): 0.96 0.96 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2852 0 0 0 5991 7 0 0 25 0 1 0 539537392 14397440 2825 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3515 2825 603 41 0 3474 0 vsize: 14060 [startup+70.0009 s] Raw data (loadavg): 0.97 0.96 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3078 0 0 0 6990 8 0 0 25 0 1 0 539537392 15331328 3051 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3743 3051 603 41 0 3702 0 vsize: 14972 [startup+80.0015 s] Raw data (loadavg): 0.97 0.96 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 7989 9 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+90.0021 s] Raw data (loadavg): 0.97 0.96 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 8989 9 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+100.002 s] Raw data (loadavg): 0.98 0.97 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 9989 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+110.002 s] Raw data (loadavg): 0.98 0.97 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 10989 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+120.003 s] Raw data (loadavg): 0.98 0.97 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 11988 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.87 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 12988 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+140.004 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15798 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 13988 11 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223552 1075349719 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 14987 12 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3170 603 41 0 3862 0 vsize: 15612 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3198 0 0 0 15987 12 0 0 25 0 1 0 539537392 15986688 3171 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3171 603 41 0 3862 0 vsize: 15612 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3198 0 0 0 16987 12 0 0 25 0 1 0 539537392 15986688 3171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3171 603 41 0 3862 0 vsize: 15612 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3198 0 0 0 17987 13 0 0 25 0 1 0 539537392 15986688 3171 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3171 603 41 0 3862 0 vsize: 15612 [startup+190.005 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3478 0 0 0 18986 14 0 0 25 0 1 0 539537392 17063936 3451 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4166 3451 603 41 0 4125 0 vsize: 16664 [startup+200.004 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3845 0 0 0 19983 16 0 0 25 0 1 0 539537392 18522112 3818 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4522 3818 603 41 0 4481 0 vsize: 18088 [startup+210.004 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4233 0 0 0 20983 17 0 0 25 0 1 0 539537392 20156416 4206 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4921 4206 603 41 0 4880 0 vsize: 19684 [startup+220.012 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 21983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4342 603 41 0 5011 0 vsize: 20208 [startup+230.013 s] Raw data (loadavg): 0.99 0.97 0.88 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 22983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4342 603 41 0 5011 0 vsize: 20208 [startup+240.015 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 23983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4342 603 41 0 5011 0 vsize: 20208 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 24983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4342 603 41 0 5011 0 vsize: 20208 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 25982 19 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4342 603 41 0 5011 0 vsize: 20208 [startup+270.015 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 26982 19 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4342 603 41 0 5011 0 vsize: 20208 [startup+280.016 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4491 0 0 0 27982 20 0 0 25 0 1 0 539537392 21233664 4464 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4464 603 41 0 5143 0 vsize: 20736 [startup+290.016 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4499 0 0 0 28981 20 0 0 25 0 1 0 539537392 21233664 4472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4472 603 41 0 5143 0 vsize: 20736 [startup+300.016 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4499 0 0 0 29981 20 0 0 25 0 1 0 539537392 21233664 4472 4294967295 134512640 134672761 3221224544 3221223680 134565039 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4472 603 41 0 5143 0 vsize: 20736 [startup+310.023 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 30982 20 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4479 603 41 0 5143 0 vsize: 20736 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 31982 21 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4479 603 41 0 5143 0 vsize: 20736 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.89 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 32983 21 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4479 603 41 0 5143 0 vsize: 20736 [startup+340.034 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 33983 21 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5184 4479 603 41 0 5143 0 vsize: 20736 [startup+350.034 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15800 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4826 0 0 0 34982 22 0 0 25 0 1 0 539537392 22564864 4799 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5509 4799 603 41 0 5468 0 vsize: 22036 [startup+360.034 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4944 0 0 0 35981 23 0 0 25 0 1 0 539537392 23101440 4917 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5640 4917 603 41 0 5599 0 vsize: 22560 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4944 0 0 0 36980 23 0 0 25 0 1 0 539537392 23101440 4917 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5640 4917 603 41 0 5599 0 vsize: 22560 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4967 0 0 0 37980 24 0 0 25 0 1 0 539537392 23240704 4940 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5674 4940 603 41 0 5633 0 vsize: 22696 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5006 0 0 0 38980 24 0 0 25 0 1 0 539537392 23404544 4979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5714 4979 603 41 0 5673 0 vsize: 22856 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5062 0 0 0 39979 25 0 0 25 0 1 0 539537392 23764992 5035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5802 5035 603 41 0 5761 0 vsize: 23208 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5062 0 0 0 40979 25 0 0 25 0 1 0 539537392 23764992 5035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5802 5035 603 41 0 5761 0 vsize: 23208 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5062 0 0 0 41979 25 0 0 25 0 1 0 539537392 23764992 5035 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5802 5035 603 41 0 5761 0 vsize: 23208 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.90 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5063 0 0 0 42979 26 0 0 25 0 1 0 539537392 23764992 5036 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5802 5036 603 41 0 5761 0 vsize: 23208 [startup+440.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5077 0 0 0 43979 26 0 0 25 0 1 0 539537392 23764992 5050 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5802 5050 603 41 0 5761 0 vsize: 23208 [startup+450.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5092 0 0 0 44978 26 0 0 25 0 1 0 539537392 23764992 5065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5802 5065 603 41 0 5761 0 vsize: 23208 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5338 0 0 0 45977 27 0 0 25 0 1 0 539537392 24825856 5311 4294967295 134512640 134672761 3221224544 3221223648 134554647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6061 5311 603 41 0 6020 0 vsize: 24244 [startup+470.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5338 0 0 0 46977 27 0 0 25 0 1 0 539537392 24825856 5311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6061 5311 603 41 0 6020 0 vsize: 24244 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5338 0 0 0 47977 28 0 0 25 0 1 0 539537392 24825856 5311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6061 5311 603 41 0 6020 0 vsize: 24244 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5341 0 0 0 48977 28 0 0 25 0 1 0 539537392 24825856 5314 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6061 5314 603 41 0 6020 0 vsize: 24244 [startup+500.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5360 0 0 0 49977 29 0 0 25 0 1 0 539537392 24961024 5333 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6094 5333 603 41 0 6053 0 vsize: 24376 [startup+510.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5371 0 0 0 50976 29 0 0 25 0 1 0 539537392 24961024 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6094 5344 603 41 0 6053 0 vsize: 24376 [startup+520.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5381 0 0 0 51976 29 0 0 25 0 1 0 539537392 25157632 5354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6142 5354 603 41 0 6101 0 vsize: 24568 [startup+530.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5389 0 0 0 52977 30 0 0 25 0 1 0 539537392 25157632 5362 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6142 5362 603 41 0 6101 0 vsize: 24568 [startup+540.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5402 0 0 0 53976 31 0 0 25 0 1 0 539537392 25157632 5375 4294967295 134512640 134672761 3221224544 3221223728 134558941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6142 5375 603 41 0 6101 0 vsize: 24568 [startup+550.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5406 0 0 0 54976 31 0 0 25 0 1 0 539537392 25157632 5379 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6142 5379 603 41 0 6101 0 vsize: 24568 [startup+560.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5407 0 0 0 55976 31 0 0 25 0 1 0 539537392 25157632 5380 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6142 5380 603 41 0 6101 0 vsize: 24568 [startup+570.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5433 0 0 0 56976 32 0 0 25 0 1 0 539537392 25354240 5406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6190 5406 603 41 0 6149 0 vsize: 24760 [startup+580.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5435 0 0 0 57976 32 0 0 25 0 1 0 539537392 25354240 5408 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6190 5408 603 41 0 6149 0 vsize: 24760 [startup+590.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5437 0 0 0 58975 32 0 0 25 0 1 0 539537392 25354240 5410 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6190 5410 603 41 0 6149 0 vsize: 24760 [startup+600.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5472 0 0 0 59975 33 0 0 25 0 1 0 539537392 25550848 5445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6238 5445 603 41 0 6197 0 vsize: 24952 [startup+610.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5536 0 0 0 60975 33 0 0 25 0 1 0 539537392 25681920 5509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6270 5509 603 41 0 6229 0 vsize: 25080 [startup+620.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5594 0 0 0 61974 34 0 0 25 0 1 0 539537392 25944064 5567 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6334 5567 603 41 0 6293 0 vsize: 25336 [startup+630.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5608 0 0 0 62974 34 0 0 25 0 1 0 539537392 26116096 5581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6376 5581 603 41 0 6335 0 vsize: 25504 [startup+640.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5637 0 0 0 63974 34 0 0 25 0 1 0 539537392 26116096 5610 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6376 5610 603 41 0 6335 0 vsize: 25504 [startup+650.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15802 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5639 0 0 0 64974 34 0 0 25 0 1 0 539537392 26116096 5612 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6376 5612 603 41 0 6335 0 vsize: 25504 [startup+660.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5659 0 0 0 65973 35 0 0 25 0 1 0 539537392 26312704 5632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6424 5632 603 41 0 6383 0 vsize: 25696 [startup+670.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5661 0 0 0 66973 35 0 0 25 0 1 0 539537392 26312704 5634 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6424 5634 603 41 0 6383 0 vsize: 25696 [startup+680.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5662 0 0 0 67973 35 0 0 25 0 1 0 539537392 26312704 5635 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6424 5635 603 41 0 6383 0 vsize: 25696 [startup+690.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5662 0 0 0 68973 36 0 0 25 0 1 0 539537392 26312704 5635 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6424 5635 603 41 0 6383 0 vsize: 25696 [startup+700.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5692 0 0 0 69973 36 0 0 25 0 1 0 539537392 26509312 5665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6472 5665 603 41 0 6431 0 vsize: 25888 [startup+710.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5714 0 0 0 70973 36 0 0 25 0 1 0 539537392 26705920 5687 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6520 5687 603 41 0 6479 0 vsize: 26080 [startup+720.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5751 0 0 0 71973 36 0 0 25 0 1 0 539537392 26841088 5724 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6553 5724 603 41 0 6512 0 vsize: 26212 [startup+730.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5751 0 0 0 72973 36 0 0 25 0 1 0 539537392 26841088 5724 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6553 5724 603 41 0 6512 0 vsize: 26212 [startup+740.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5754 0 0 0 73973 36 0 0 25 0 1 0 539537392 26841088 5727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6553 5727 603 41 0 6512 0 vsize: 26212 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5761 0 0 0 74972 37 0 0 25 0 1 0 539537392 26841088 5734 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6553 5734 603 41 0 6512 0 vsize: 26212 [startup+760.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5778 0 0 0 75973 37 0 0 25 0 1 0 539537392 27021312 5751 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6597 5751 603 41 0 6556 0 vsize: 26388 [startup+770.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5784 0 0 0 76974 38 0 0 25 0 1 0 539537392 27021312 5757 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6597 5757 603 41 0 6556 0 vsize: 26388 [startup+780.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5806 0 0 0 77974 38 0 0 25 0 1 0 539537392 27021312 5779 4294967295 134512640 134672761 3221224544 3221223728 134558880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6597 5779 603 41 0 6556 0 vsize: 26388 [startup+790.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5808 0 0 0 78977 39 0 0 25 0 1 0 539537392 27021312 5781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6597 5781 603 41 0 6556 0 vsize: 26388 [startup+800.134 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5809 0 0 0 79976 39 0 0 25 0 1 0 539537392 27021312 5782 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6597 5782 603 41 0 6556 0 vsize: 26388 [startup+810.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5836 0 0 0 80977 39 0 0 25 0 1 0 539537392 27283456 5809 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6661 5809 603 41 0 6620 0 vsize: 26644 [startup+820.341 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5866 0 0 0 81997 39 0 0 25 0 1 0 539537392 27283456 5839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6661 5839 603 41 0 6620 0 vsize: 26644 [startup+830.342 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6010 0 0 0 82997 40 0 0 25 0 1 0 539537392 28078080 5983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6855 5983 603 41 0 6814 0 vsize: 27420 [startup+840.342 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6138 0 0 0 83996 41 0 0 25 0 1 0 539537392 28741632 6111 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7017 6111 603 41 0 6976 0 vsize: 28068 [startup+850.346 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6140 0 0 0 84996 41 0 0 25 0 1 0 539537392 28741632 6113 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7017 6113 603 41 0 6976 0 vsize: 28068 [startup+860.346 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6140 0 0 0 85996 41 0 0 25 0 1 0 539537392 28741632 6113 4294967295 134512640 134672761 3221224544 3221223728 134559055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7017 6113 603 41 0 6976 0 vsize: 28068 [startup+870.346 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6146 0 0 0 86995 42 0 0 25 0 1 0 539537392 28741632 6119 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7017 6119 603 41 0 6976 0 vsize: 28068 [startup+880.376 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6152 0 0 0 87998 42 0 0 25 0 1 0 539537392 28741632 6125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7017 6125 603 41 0 6976 0 vsize: 28068 [startup+890.376 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6153 0 0 0 88999 42 0 0 25 0 1 0 539537392 28741632 6126 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7017 6126 603 41 0 6976 0 vsize: 28068 [startup+900.377 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6171 0 0 0 89998 42 0 0 25 0 1 0 539537392 29003776 6144 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7081 6144 603 41 0 7040 0 vsize: 28324 [startup+910.378 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6198 0 0 0 90989 43 0 0 25 0 1 0 539537392 29003776 6171 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7081 6171 603 41 0 7040 0 vsize: 28324 [startup+920.379 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6198 0 0 0 91989 43 0 0 25 0 1 0 539537392 29003776 6171 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7081 6171 603 41 0 7040 0 vsize: 28324 [startup+930.379 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6198 0 0 0 92989 43 0 0 25 0 1 0 539537392 29003776 6171 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7081 6171 603 41 0 7040 0 vsize: 28324 [startup+940.379 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6495 0 0 0 93988 44 0 0 25 0 1 0 539537392 30220288 6468 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7378 6468 603 41 0 7337 0 vsize: 29512 [startup+950.38 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15804 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6757 0 0 0 94987 46 0 0 25 0 1 0 539537392 31289344 6730 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7639 6730 603 41 0 7598 0 vsize: 30556 [startup+960.38 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 95987 46 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7639 6731 603 41 0 7598 0 vsize: 30556 [startup+970.379 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 96986 47 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7639 6731 603 41 0 7598 0 vsize: 30556 [startup+980.387 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 97987 47 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7639 6731 603 41 0 7598 0 vsize: 30556 [startup+990.387 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 98986 48 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7639 6731 603 41 0 7598 0 vsize: 30556 [startup+1000.39 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 99986 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6746 603 41 0 7640 0 vsize: 30724 [startup+1010.39 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 100986 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6746 603 41 0 7640 0 vsize: 30724 [startup+1020.4 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 101987 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6746 603 41 0 7640 0 vsize: 30724 [startup+1030.42 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 102989 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6746 603 41 0 7640 0 vsize: 30724 [startup+1040.42 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 103989 49 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6746 603 41 0 7640 0 vsize: 30724 [startup+1050.43 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6774 0 0 0 104990 49 0 0 25 0 1 0 539537392 31461376 6747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6747 603 41 0 7640 0 vsize: 30724 [startup+1060.43 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6777 0 0 0 105990 49 0 0 25 0 1 0 539537392 31461376 6750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6750 603 41 0 7640 0 vsize: 30724 [startup+1070.45 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6792 0 0 0 106990 50 0 0 25 0 1 0 539537392 31461376 6765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7681 6765 603 41 0 7640 0 vsize: 30724 [startup+1080.45 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 107990 50 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1090.45 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 108990 50 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1100.46 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 109991 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1110.47 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 110991 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1120.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 111993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1130.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 112993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1140.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 113993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1150.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 114993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1160.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 115994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1170.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 116994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1180.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 117994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1190.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 118994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 [startup+1200.49 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15806 Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 119994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6782 603 41 0 7688 0 vsize: 30916 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.51 s] Raw data (loadavg): 0.99 0.97 0.91 1/55 15806 Raw data (stat): 15796 (minisat+) Z 15795 20838 20837 0 -1 12 6812 0 0 0 119995 52 0 0 25 0 1 0 539537392 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.51 CPU time (s): 1200.48 CPU user time (s): 1199.95 CPU system time (s): 0.526919 CPU usage (%): 99.9975 Max. virtual memory (Kb): 30916 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####