Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb |
MD5SUM | a89f4ed95903fddf213992506514bcf0 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 16 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 906 |
Biggest coefficient in the objective function | 553 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 2526 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 553 |
Number of bits of the biggest number in a constraint | 10 |
Biggest sum of numbers in a constraint | 2526 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04184 |
Number of variables | 906 |
Total number of constraints | 1944 |
Number of constraints which are clauses | 852 |
Number of constraints which are cardinality constraints (but not clauses) | 1092 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 18 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc17 THE 2005-04-14 03:15:19 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4507 boxname=wulflinc17 idbench=371 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a89f4ed95903fddf213992506514bcf0 /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb IDLAUNCH: 4507 /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: 820064 kB Buffers: 35984 kB Cached: 143812 kB SwapCached: 2376 kB Active: 58944 kB Inactive: 126212 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 819812 kB SwapTotal: 2097892 kB SwapFree: 2095516 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7036 kB Slab: 23736 kB Committed_AS: 63708 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 03:35:22 (client local time) WITH STATUS 10 IN 1200.23 SECONDS stats: 4507 7 1200.23 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1038 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 187]---> BDD-cost: 5 c ---[ 186]---> BDD-cost: 8 c ---[ 185]---> BDD-cost: 14 c ---[ 184]---> BDD-cost: 14 c ---[ 183]---> BDD-cost: 17 c ---[ 182]---> BDD-cost: 14 c ---[ 181]---> BDD-cost: 23 c ---[ 180]---> BDD-cost: 20 c ---[ 179]---> BDD-cost: 29 c ---[ 178]---> BDD-cost: 29 c ---[ 177]---> BDD-cost: 38 c ---[ 176]---> BDD-cost: 32 c ---[ 175]---> BDD-cost: 32 c ---[ 174]---> BDD-cost: 23 c ---[ 173]---> BDD-cost: 26 c ---[ 172]---> BDD-cost: 20 c ---[ 171]---> BDD-cost: 20 c ---[ 170]---> BDD-cost: 14 c ---[ 169]---> BDD-cost: 14 c ---[ 168]---> BDD-cost: 8 c ---[ 167]---> BDD-cost: 8 c ---[ 166]---> BDD-cost: 11 c ---[ 165]---> BDD-cost: 14 c ---[ 164]---> BDD-cost: 17 c ---[ 163]---> BDD-cost: 18 c ---[ 162]---> BDD-cost: 18 c ---[ 161]---> BDD-cost: 35 c ---[ 160]---> BDD-cost: 35 c ---[ 159]---> BDD-cost: 41 c ---[ 158]---> BDD-cost: 35 c ---[ 157]---> BDD-cost: 38 c ---[ 156]---> BDD-cost: 38 c ---[ 155]---> BDD-cost: 41 c ---[ 154]---> BDD-cost: 35 c ---[ 153]---> BDD-cost: 38 c ---[ 152]---> BDD-cost: 23 c ---[ 151]---> BDD-cost: 20 c ---[ 150]---> BDD-cost: 17 c ---[ 149]---> BDD-cost: 20 c ---[ 148]---> BDD-cost: 11 c ---[ 147]---> BDD-cost: 8 c ---[ 146]---> BDD-cost: 11 c ---[ 145]---> BDD-cost: 14 c ---[ 144]---> BDD-cost: 17 c ---[ 143]---> BDD-cost: 23 c ---[ 142]---> BDD-cost: 29 c ---[ 141]---> BDD-cost: 41 c ---[ 140]---> BDD-cost: 44 c ---[ 139]---> BDD-cost: 44 c ---[ 138]---> BDD-cost: 38 c ---[ 137]---> BDD-cost: 39 c ---[ 136]---> BDD-cost: 41 c ---[ 135]---> BDD-cost: 44 c ---[ 134]---> BDD-cost: 44 c ---[ 133]---> BDD-cost: 41 c ---[ 132]---> BDD-cost: 29 c ---[ 131]---> BDD-cost: 29 c ---[ 130]---> BDD-cost: 23 c ---[ 129]---> BDD-cost: 26 c ---[ 128]---> BDD-cost: 14 c ---[ 127]---> BDD-cost: 8 c ---[ 126]---> BDD-cost: 11 c ---[ 125]---> BDD-cost: 14 c ---[ 124]---> BDD-cost: 17 c ---[ 123]---> BDD-cost: 21 c ---[ 122]---> BDD-cost: 29 c ---[ 121]---> BDD-cost: 35 c ---[ 120]---> BDD-cost: 44 c ---[ 119]---> BDD-cost: 47 c ---[ 118]---> BDD-cost: 44 c ---[ 117]---> BDD-cost: 44 c ---[ 116]---> BDD-cost: 44 c ---[ 115]---> BDD-cost: 41 c ---[ 114]---> BDD-cost: 38 c ---[ 113]---> BDD-cost: 35 c ---[ 112]---> BDD-cost: 32 c ---[ 111]---> BDD-cost: 29 c ---[ 110]---> BDD-cost: 26 c ---[ 109]---> BDD-cost: 20 c ---[ 108]---> BDD-cost: 6 c ---[ 107]---> BDD-cost: 5 c ---[ 106]---> BDD-cost: 14 c ---[ 105]---> BDD-cost: 20 c ---[ 104]---> BDD-cost: 23 c ---[ 103]---> BDD-cost: 26 c ---[ 102]---> BDD-cost: 35 c ---[ 101]---> BDD-cost: 38 c ---[ 100]---> BDD-cost: 35 c ---[ 99]---> BDD-cost: 41 c ---[ 98]---> BDD-cost: 44 c ---[ 97]---> BDD-cost: 41 c ---[ 96]---> BDD-cost: 38 c ---[ 95]---> BDD-cost: 41 c ---[ 94]---> BDD-cost: 38 c ---[ 93]---> BDD-cost: 29 c ---[ 92]---> BDD-cost: 20 c ---[ 91]---> BDD-cost: 26 c ---[ 90]---> BDD-cost: 20 c ---[ 89]---> BDD-cost: 14 c ---[ 88]---> BDD-cost: 5 c ---[ 87]---> BDD-cost: 5 c ---[ 86]---> BDD-cost: 11 c ---[ 85]---> BDD-cost: 20 c ---[ 84]---> BDD-cost: 20 c ---[ 83]---> BDD-cost: 32 c ---[ 82]---> BDD-cost: 41 c ---[ 81]---> BDD-cost: 38 c ---[ 80]---> BDD-cost: 35 c ---[ 79]---> BDD-cost: 32 c ---[ 78]---> BDD-cost: 35 c ---[ 77]---> BDD-cost: 44 c ---[ 76]---> BDD-cost: 35 c ---[ 75]---> BDD-cost: 38 c ---[ 74]---> BDD-cost: 35 c ---[ 73]---> BDD-cost: 29 c ---[ 72]---> BDD-cost: 23 c ---[ 71]---> BDD-cost: 17 c ---[ 70]---> BDD-cost: 17 c ---[ 69]---> BDD-cost: 11 c ---[ 68]---> BDD-cost: 3 c ---[ 67]---> BDD-cost: 7 c ---[ 66]---> BDD-cost: 11 c ---[ 65]---> BDD-cost: 17 c ---[ 64]---> BDD-cost: 23 c ---[ 63]---> BDD-cost: 32 c ---[ 62]---> BDD-cost: 26 c ---[ 61]---> BDD-cost: 38 c ---[ 60]---> BDD-cost: 32 c ---[ 59]---> BDD-cost: 32 c ---[ 58]---> BDD-cost: 35 c ---[ 57]---> BDD-cost: 38 c ---[ 56]---> BDD-cost: 32 c ---[ 55]---> BDD-cost: 35 c ---[ 54]---> BDD-cost: 29 c ---[ 53]---> BDD-cost: 32 c ---[ 52]---> BDD-cost: 29 c ---[ 51]---> BDD-cost: 23 c ---[ 50]---> BDD-cost: 17 c ---[ 49]---> BDD-cost: 11 c ---[ 47]---> BDD-cost: 8 c ---[ 46]---> BDD-cost: 20 c ---[ 45]---> BDD-cost: 14 c ---[ 44]---> BDD-cost: 17 c ---[ 43]---> BDD-cost: 20 c ---[ 42]---> BDD-cost: 20 c ---[ 41]---> BDD-cost: 35 c ---[ 40]---> BDD-cost: 35 c ---[ 39]---> BDD-cost: 35 c ---[ 38]---> BDD-cost: 23 c ---[ 37]---> BDD-cost: 26 c ---[ 36]---> BDD-cost: 23 c ---[ 35]---> BDD-cost: 23 c ---[ 34]---> BDD-cost: 23 c ---[ 33]---> BDD-cost: 26 c ---[ 32]---> BDD-cost: 17 c ---[ 31]---> BDD-cost: 5 c ---[ 30]---> BDD-cost: 8 c ---[ 29]---> BDD-cost: 14 c ---[ 28]---> BDD-cost: 14 c ---[ 27]---> BDD-cost: 14 c ---[ 26]---> BDD-cost: 26 c ---[ 25]---> BDD-cost: 20 c ---[ 24]---> BDD-cost: 26 c ---[ 23]---> BDD-cost: 17 c ---[ 22]---> BDD-cost: 15 c ---[ 21]---> BDD-cost: 20 c ---[ 20]---> BDD-cost: 20 c ---[ 19]---> BDD-cost: 17 c ---[ 18]---> BDD-cost: 20 c ---[ 17]---> BDD-cost: 11 c ---[ 16]---> BDD-cost: 8 c ---[ 14]---> BDD-cost: 7 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 14 c ---[ 11]---> BDD-cost: 11 c ---[ 10]---> BDD-cost: 17 c ---[ 9]---> BDD-cost: 14 c ---[ 8]---> BDD-cost: 14 c ---[ 7]---> BDD-cost: 14 c ---[ 6]---> BDD-cost: 14 c ---[ 5]---> BDD-cost: 14 c ---[ 4]---> BDD-cost: 17 c ---[ 3]---> BDD-cost: 14 c ---[ 2]---> BDD-cost: 14 c ---[ 1]---> BDD-cost: 8 c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11181 31975 | 3727 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 959[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:69497 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 98065 235598 | 32688 0 0 nan | 0.000 % | c | 100 | 97945 235356 | 35956 96 1183 12.3 | 0.394 % | c ============================================================================== c [1mFound solution: 132[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 131 | 136862 326344 | 45620 126 1575 12.5 | 0.394 % | c | 231 | 136649 325872 | 50182 222 2400 10.8 | 0.554 % | c | 381 | 136566 325685 | 55200 371 4150 11.2 | 0.591 % | c | 606 | 136566 325685 | 60720 596 6346 10.6 | 0.591 % | c | 943 | 136566 325685 | 66792 933 8111 8.7 | 0.591 % | c | 1449 | 136434 325390 | 73471 1437 14754 10.3 | 0.671 % | c | 2209 | 136345 325187 | 80818 2196 31136 14.2 | 0.712 % | c | 3348 | 135750 323871 | 88900 3322 50719 15.3 | 1.106 % | c | 5058 | 135114 322442 | 97790 5020 71012 14.1 | 1.471 % | c | 7620 | 134367 320766 | 107569 7476 135375 18.1 | 1.979 % | c | 11465 | 134060 320072 | 118326 11311 205024 18.1 | 2.171 % | c | 17232 | 133659 319161 | 130159 17043 364167 21.4 | 2.450 % | c | 25881 | 133659 319161 | 143175 25692 627411 24.4 | 2.450 % | c ============================================================================== c [1mFound solution: 100[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34908 | 133443 318742 | 44481 34692 882375 25.4 | 2.450 % | c | 35008 | 133443 318742 | 48929 34792 883822 25.4 | 2.667 % | c | 35159 | 133083 317915 | 53822 34933 885011 25.3 | 2.897 % | c | 35384 | 132785 317236 | 59204 34989 885325 25.3 | 3.066 % | c | 35721 | 132785 317236 | 65124 35326 890308 25.2 | 3.066 % | c | 36228 | 132785 317236 | 71637 35833 900634 25.1 | 3.066 % | c | 36990 | 132671 316976 | 78800 36592 911872 24.9 | 3.121 % | c | 38129 | 132671 316976 | 86680 37731 957809 25.4 | 3.121 % | c | 39838 | 132671 316976 | 95348 39440 1007183 25.5 | 3.121 % | c | 42403 | 132671 316976 | 104883 42005 1047666 24.9 | 3.121 % | c ============================================================================== c [1mFound solution: 89[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45719 | 132741 317174 | 44247 45321 1112617 24.5 | 3.121 % | c | 45820 | 132741 317174 | 48671 45422 1114217 24.5 | 3.120 % | c | 45970 | 132681 317044 | 53538 45566 1116344 24.5 | 3.173 % | c | 46196 | 132539 316726 | 58892 45787 1120083 24.5 | 3.267 % | c | 46535 | 132539 316726 | 64782 46126 1124906 24.4 | 3.267 % | c | 47042 | 132530 316707 | 71260 46630 1144255 24.5 | 3.274 % | c | 47803 | 132530 316707 | 78386 47391 1163560 24.6 | 3.274 % | c | 48943 | 132530 316707 | 86224 48531 1185721 24.4 | 3.274 % | c | 50652 | 132530 316707 | 94847 50240 1229199 24.5 | 3.274 % | c | 53214 | 132528 316703 | 104332 52800 1342600 25.4 | 3.276 % | c | 57058 | 132524 316695 | 114765 56636 1423156 25.1 | 3.279 % | c | 62824 | 132524 316695 | 126241 62402 1547383 24.8 | 3.279 % | c | 71475 | 132520 316686 | 138866 71048 1961678 27.6 | 3.280 % | c | 84449 | 132505 316652 | 152752 84019 2524728 30.0 | 3.292 % | c ============================================================================== c [1mFound solution: 71[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 85791 | 132621 316968 | 44207 85361 2565105 30.1 | 3.292 % | c | 85892 | 132621 316968 | 48627 20576 545228 26.5 | 3.290 % | c | 86042 | 132621 316968 | 53490 20726 546710 26.4 | 3.290 % | c | 86267 | 132621 316968 | 58839 20951 548910 26.2 | 3.290 % | c | 86604 | 132621 316968 | 64723 21288 553079 26.0 | 3.290 % | c | 87110 | 132621 316968 | 71195 21794 583363 26.8 | 3.290 % | c | 87869 | 132621 316968 | 78315 22553 598604 26.5 | 3.290 % | c | 89008 | 132584 316891 | 86146 23691 622554 26.3 | 3.320 % | c | 90716 | 132584 316891 | 94761 25399 650846 25.6 | 3.320 % | c | 93278 | 132584 316891 | 104237 27961 724322 25.9 | 3.320 % | c | 97123 | 132584 316891 | 114661 31806 1075400 33.8 | 3.320 % | c | 102889 | 132584 316891 | 126127 37572 1291066 34.4 | 3.320 % | c | 111538 | 132584 316891 | 138740 46221 2350342 50.9 | 3.320 % | c | 124514 | 132584 316891 | 152614 59197 4144544 70.0 | 3.320 % | c ============================================================================== c [1mFound solution: 68[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 126224 | 132591 316914 | 44197 60907 4187539 68.8 | 3.320 % | c | 126324 | 132591 316914 | 48616 19936 1802665 90.4 | 3.322 % | c | 126476 | 132591 316914 | 53478 20088 1805539 89.9 | 3.322 % | c | 126701 | 132591 316914 | 58826 20313 1811155 89.2 | 3.322 % | c | 127039 | 132591 316914 | 64708 20651 1832976 88.8 | 3.322 % | c | 127545 | 132591 316914 | 71179 21157 1836496 86.8 | 3.322 % | c | 128304 | 132591 316914 | 78297 21916 1865065 85.1 | 3.322 % | c | 129443 | 132591 316914 | 86127 23055 1888123 81.9 | 3.322 % | c | 131151 | 132591 316914 | 94740 24763 1983029 80.1 | 3.322 % | c | 133713 | 132591 316914 | 104214 27325 2024838 74.1 | 3.322 % | c | 137557 | 132591 316914 | 114635 31169 2136748 68.6 | 3.322 % | c | 143323 | 132591 316914 | 126099 36935 4189369 113.4 | 3.322 % | c | 151972 | 132587 316905 | 138709 45581 4407036 96.7 | 3.323 % | c | 164947 | 132465 316619 | 152580 58555 5024064 85.8 | 3.412 % | c | 184412 | 132465 316619 | 167838 78020 7623876 97.7 | 3.412 % | c ============================================================================== c [1mFound solution: 67[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 197095 | 132301 316262 | 44100 90701 8886122 98.0 | 3.412 % | c | 197195 | 132301 316262 | 48510 24436 1360111 55.7 | 3.537 % | c | 197345 | 132301 316262 | 53361 24586 1364199 55.5 | 3.537 % | c | 197571 | 132290 316239 | 58697 24807 1374683 55.4 | 3.546 % | c | 197910 | 132290 316239 | 64566 25146 1379093 54.8 | 3.546 % | c | 198416 | 132290 316239 | 71023 25652 1446731 56.4 | 3.546 % | c | 199176 | 132290 316239 | 78125 26412 1468692 55.6 | 3.546 % | c | 200315 | 132290 316239 | 85938 27551 1522689 55.3 | 3.546 % | c | 202023 | 132290 316239 | 94532 29259 1580387 54.0 | 3.546 % | c | 204585 | 132290 316239 | 103985 31821 1650237 51.9 | 3.546 % | c | 208430 | 132290 316239 | 114384 35666 1784724 50.0 | 3.546 % | c | 214196 | 132290 316239 | 125822 41432 2360684 57.0 | 3.546 % | c | 222845 | 132290 316239 | 138404 50081 6002993 119.9 | 3.546 % | c ============================================================================== c [1mFound solution: 63[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 229804 | 132292 316270 | 44097 57035 6339200 111.1 | 3.546 % | c | 229905 | 132292 316270 | 48506 22974 2901498 126.3 | 3.573 % | c | 230055 | 132292 316270 | 53357 23124 2904349 125.6 | 3.573 % | c | 230280 | 132292 316270 | 58693 23349 2909964 124.6 | 3.573 % | c | 230618 | 132292 316270 | 64562 23687 2925173 123.5 | 3.573 % | c | 231124 | 132292 316270 | 71018 24193 2933205 121.2 | 3.573 % | c | 231883 | 132292 316270 | 78120 24952 2949533 118.2 | 3.573 % | c | 233022 | 132292 316270 | 85932 26091 2971394 113.9 | 3.573 % | c | 234731 | 132292 316270 | 94525 27800 3013791 108.4 | 3.573 % | c | 237293 | 132292 316270 | 103978 30362 3199427 105.4 | 3.573 % | c | 241138 | 132292 316270 | 114376 34207 3342197 97.7 | 3.573 % | c | 246904 | 132270 316220 | 125813 39965 3636032 91.0 | 3.582 % | c | 255553 | 132270 316220 | 138395 48614 4093710 84.2 | 3.582 % | c | 268527 | 132242 316154 | 152234 61582 7533973 122.3 | 3.611 % | c | 287989 | 132239 316147 | 167458 81040 8673069 107.0 | 3.614 % | c | 317182 | 132239 316147 | 184204 110233 9873954 89.6 | 3.614 % | c c *** TERMINATED *** s SATISFIABLE v -v785 v740 v420 v82 -v860 v744 v418 v859 -v784 -v501 v307 -v85 -v788 v419 -v86 -v63 v861 -v504 -v424 -v354 v306 v62 v863 -v789 -v573 -v505 v64 -v572 -v478 v441 -v353 -v312 v65 -v27 -v864 -v574 -v477 -v310 v102 v66 v866 -v810 -v575 -v479 v440 -v359 -v262 -v185 v101 -v73 -v26 v867 -v814 -v576 -v482 -v357 -v311 -v190 -v107 v67 -v30 -v697 -v583 v481 -v446 v399 -v315 -v265 -v216 -v189 v143 -v106 -v68 -v701 -v577 v486 -v444 -v358 -v266 v142 -v108 -v69 -v31 -v2 -v578 v485 v398 -v362 -v192 -v166 v144 -v112 -v1 -v660 -v579 -v483 -v445 -v193 v147 -v111 v7 -v659 -v594 -v558 -v484 -v449 -v404 v196 -v165 v146 -v109 v6 -v661 -v598 -v557 -v402 v194 v151 -v110 v8 -v662 -v559 -v332 v195 -v171 v150 v12 v663 -v562 -v403 -v169 v148 v11 v668 v561 -v407 -v335 v149 v9 v664 v563 -v336 -v170 v10 v739 v421 v81 -v855 v743 -v854 -v786 -v500 v425 -v302 v87 -v790 -v423 v862 -v506 -v349 v308 v865 v869 -v835 v792 -v436 -v355 -v313 v90 -v76 v868 -v839 v793 -v77 -v809 -v586 -v509 v442 -v360 -v316 -v261 -v212 -v72 -v28 -v813 -v587 -v480 -v314 -v184 v103 -v32 -v696 -v582 v494 v447 -v394 -v363 -v267 -v215 -v186 v104 -v70 -v700 v490 -v361 -v191 v105 -v580 v489 v450 v400 v188 -v161 -v116 -v34 v448 v197 v145 -v35 -v3 -v593 -v542 v405 -v270 -v167 v159 v4 -v597 v155 v5 -v671 v408 -v331 -v172 v154 -v16 -v672 -v560 v406 v667 -v571 -v466 -v337 -v173 v567 -v470 -v174 v781 v741 -v496 v422 v83 v745 v426 v787 -v502 v88 v856 v791 -v301 v857 v795 -v747 -v507 -v303 v91 -v75 v858 v794 -v748 -v348 v309 v89 -v74 -v22 v873 -v834 -v761 -v585 -v510 -v350 v305 -v257 -v21 -v838 -v765 -v584 -v508 -v435 -v356 -v317 -v811 v491 -v437 v352 -v263 -v211 -v29 -v815 v493 v443 -v364 -v33 -v698 v439 -v268 -v217 -v119 -v71 -v37 -v702 v451 -v393 -v187 -v120 -v36 -v817 -v581 -v538 v487 -v395 -v271 v205 v156 -v115 -v818 v401 -v269 v201 -v160 v158 -v704 -v670 -v595 -v541 v488 v397 -v327 -v220 v200 -v162 -v113 -v19 -v705 -v669 -v599 v409 -v168 -v20 -v722 -v568 -v333 -v164 v152 -v15 v726 -v570 -v175 v665 -v601 -v465 -v338 v153 v131 -v13 -v602 v566 -v469 v742 v434 -v79 v780 v746 -v495 v430 v84 v782 -v750 -v497 v429 v80 v783 -v749 -v503 v92 v876 v799 -v499 v877 -v805 -v511 -v304 v872 -v836 -v804 -v760 -v325 -v207 -v840 -v764 -v692 v492 -v351 -v321 -v256 -v23 -v884 v870 -v812 -v691 v372 -v320 -v258 -v213 -v118 -v24 -v888 -v816 -v438 v368 -v264 -v117 -v25 -v842 -v820 -v699 -v459 v367 -v260 -v218 v202 -v41 -v843 -v819 -v703 v589 -v455 -v272 v204 v157 -v707 v588 v537 -v454 -v221 -v18 -v706 -v396 -v219 -v17 -v596 -v543 -v417 v198 -v114 -v600 -v569 v413 -v326 -v163 -v721 v604 v412 -v328 -v199 -v183 -v127 v725 -v603 -v334 -v179 v666 -v546 -v467 -v330 -v178 v130 -v14 -v564 -v471 -v339 v903 v433 -v78 v875 v802 -v754 v427 -v100 v874 -v830 v803 -v498 -v96 -v829 v798 -v519 v428 -v322 -v95 -v515 -v324 -v837 v796 -v762 -v514 v369 -v841 -v806 v766 v371 -v206 -v883 v871 -v845 -v807 -v456 -v318 -v291 -v208 -v44 -v887 -v844 -v808 -v693 -v458 -v259 -v214 v203 -v45 -v824 v768 -v694 -v533 -v383 v365 -v319 -v280 -v210 -v40 v769 -v695 -v276 -v222 -v711 -v619 v539 -v452 -v414 v366 -v275 -v38 -v623 v590 -v416 v591 v544 -v453 -v180 v592 -v461 -v182 -v723 v608 v547 -v460 v410 -v126 v727 v545 -v329 -v468 v411 -v347 -v176 v132 -v565 v472 -v343 v801 v431 -v97 v800 -v99 -v753 v654 -v516 -v756 -v518 -v323 -v755 -v751 v521 -v93 -v831 -v525 v370 -v832 v797 -v763 -v512 -v287 -v249 -v94 -v43 v833 v767 -v457 -v42 -v885 v849 -v827 v771 -v513 -v379 -v290 -v277 v889 -v828 v770 -v279 -v209 -v823 -v714 -v382 -v230 -v715 -v532 -v415 -v226 -v891 -v821 -v710 v641 -v618 -v534 -v273 -v225 -v39 -v892 -v717 v645 -v622 v540 -v181 -v716 -v708 -v679 -v611 v536 -v274 -v122 v55 v683 -v612 v548 -v724 -v607 -v344 -v128 v728 -v462 -v346 v729 -v605 v463 -v240 -v177 v133 v730 v464 -v342 v904 v432 -v98 -v517 v653 -v752 v520 v245 -v879 -v757 -v524 -v878 -v852 -v826 v758 v286 v248 -v853 -v825 v759 -v278 v886 -v848 v775 -v713 -v378 -v292 -v227 v890 -v712 -v229 v894 -v846 -v384 -v893 -v822 v640 -v620 -v610 v295 -v223 v51 v644 -v624 -v609 v535 -v709 -v678 v556 -v387 -v224 v54 -v718 v682 -v552 -v345 -v121 -v719 -v626 -v551 -#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.85 0.95 0.90 2/55 28243 Raw data (stat): 28243 (runsolver) R 28242 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481281060 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.0006 s] Raw data (loadavg): 0.87 0.95 0.90 2/55 28243 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 5549 0 0 0 984 13 0 0 25 0 1 0 481281060 29401088 5371 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7178 5371 603 41 0 7137 0 vsize: 28712 [startup+20.0018 s] Raw data (loadavg): 0.89 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 5692 0 0 0 1982 15 0 0 25 0 1 0 481281060 29982720 5514 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7320 5514 603 41 0 7279 0 vsize: 29280 [startup+30.0024 s] Raw data (loadavg): 0.91 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 5823 0 0 0 2982 16 0 0 25 0 1 0 481281060 30523392 5645 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7452 5645 603 41 0 7411 0 vsize: 29808 [startup+40.0024 s] Raw data (loadavg): 0.92 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6006 0 0 0 3981 17 0 0 25 0 1 0 481281060 31285248 5828 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7638 5828 603 41 0 7597 0 vsize: 30552 [startup+50.0026 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6220 0 0 0 4980 18 0 0 25 0 1 0 481281060 32096256 6042 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7836 6042 603 41 0 7795 0 vsize: 31344 [startup+60.0022 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6395 0 0 0 5979 19 0 0 25 0 1 0 481281060 32903168 6217 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8033 6217 603 41 0 7992 0 vsize: 32132 [startup+70.0033 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6580 0 0 0 6977 21 0 0 25 0 1 0 481281060 33705984 6402 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8229 6402 603 41 0 8188 0 vsize: 32916 [startup+80.0034 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6721 0 0 0 7977 21 0 0 25 0 1 0 481281060 34217984 6543 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8354 6543 603 41 0 8313 0 vsize: 33416 [startup+90.003 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6897 0 0 0 8976 22 0 0 25 0 1 0 481281060 34889728 6719 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8518 6719 603 41 0 8477 0 vsize: 34072 [startup+100.004 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7021 0 0 0 9976 23 0 0 25 0 1 0 481281060 35409920 6843 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8645 6843 603 41 0 8604 0 vsize: 34580 [startup+110.004 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7184 0 0 0 10975 24 0 0 25 0 1 0 481281060 36085760 7006 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8810 7006 603 41 0 8769 0 vsize: 35240 [startup+120.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7350 0 0 0 11973 25 0 0 25 0 1 0 481281060 36761600 7172 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8975 7172 603 41 0 8934 0 vsize: 35900 [startup+130.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7467 0 0 0 12972 26 0 0 25 0 1 0 481281060 37163008 7289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9073 7289 603 41 0 9032 0 vsize: 36292 [startup+140.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7599 0 0 0 13972 26 0 0 25 0 1 0 481281060 37699584 7421 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9204 7421 603 41 0 9163 0 vsize: 36816 [startup+150.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7826 0 0 0 14971 27 0 0 25 0 1 0 481281060 38907904 7648 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9499 7648 603 41 0 9458 0 vsize: 37996 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8081 0 0 0 15970 28 0 0 25 0 1 0 481281060 39976960 7903 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9760 7903 603 41 0 9719 0 vsize: 39040 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8232 0 0 0 16970 29 0 0 25 0 1 0 481281060 40513536 8054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9891 8054 603 41 0 9850 0 vsize: 39564 [startup+180.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8371 0 0 0 17970 29 0 0 25 0 1 0 481281060 41046016 8193 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10021 8193 603 41 0 9980 0 vsize: 40084 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8537 0 0 0 18970 29 0 0 25 0 1 0 481281060 41840640 8359 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10215 8359 603 41 0 10174 0 vsize: 40860 [startup+200.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8674 0 0 0 19969 30 0 0 25 0 1 0 481281060 42377216 8496 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10346 8496 603 41 0 10305 0 vsize: 41384 [startup+210.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 20969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 21969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+230.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 22969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+240.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 23969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+250.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 24969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+260.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 25969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 26970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+280.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 27970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+290.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 28970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+300.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 29970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8633 603 41 0 10430 0 vsize: 41884 [startup+310.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28245 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8816 0 0 0 30970 31 0 0 25 0 1 0 481281060 42889216 8638 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10471 8638 603 41 0 10430 0 vsize: 41884 [startup+320.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 9108 0 0 0 31969 32 0 0 25 0 1 0 481281060 44101632 8930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10767 8930 603 41 0 10726 0 vsize: 43068 [startup+330.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 9486 0 0 0 32968 33 0 0 25 0 1 0 481281060 45584384 9308 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11129 9308 603 41 0 11088 0 vsize: 44516 [startup+340.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 9907 0 0 0 33968 34 0 0 25 0 1 0 481281060 47321088 9729 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11553 9729 603 41 0 11512 0 vsize: 46212 [startup+350.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10333 0 0 0 34967 35 0 0 25 0 1 0 481281060 49065984 10155 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11979 10155 603 41 0 11938 0 vsize: 47916 [startup+360.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10510 0 0 0 35966 36 0 0 25 0 1 0 481281060 49852416 10332 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10332 603 41 0 12130 0 vsize: 48684 [startup+370.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10510 0 0 0 36966 36 0 0 25 0 1 0 481281060 49852416 10332 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10332 603 41 0 12130 0 vsize: 48684 [startup+380.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 37966 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10334 603 41 0 12130 0 vsize: 48684 [startup+390.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 38966 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10334 603 41 0 12130 0 vsize: 48684 [startup+400.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 39967 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10334 603 41 0 12130 0 vsize: 48684 [startup+410.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 40967 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10334 603 41 0 12130 0 vsize: 48684 [startup+420.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 41967 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223648 134560332 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12171 10334 603 41 0 12130 0 vsize: 48684 [startup+430.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10829 0 0 0 42966 37 0 0 25 0 1 0 481281060 51191808 10651 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12498 10651 603 41 0 12457 0 vsize: 49992 [startup+440.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10831 0 0 0 43966 38 0 0 25 0 1 0 481281060 51191808 10653 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12498 10653 603 41 0 12457 0 vsize: 49992 [startup+450.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10832 0 0 0 44966 38 0 0 25 0 1 0 481281060 51191808 10654 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12498 10654 603 41 0 12457 0 vsize: 49992 [startup+460.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10949 0 0 0 45966 38 0 0 25 0 1 0 481281060 51589120 10771 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12595 10771 603 41 0 12554 0 vsize: 50380 [startup+470.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11089 0 0 0 46965 39 0 0 25 0 1 0 481281060 52252672 10911 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12757 10911 603 41 0 12716 0 vsize: 51028 [startup+480.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11316 0 0 0 47965 40 0 0 25 0 1 0 481281060 53194752 11138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12987 11138 603 41 0 12946 0 vsize: 51948 [startup+490.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11479 0 0 0 48964 40 0 0 25 0 1 0 481281060 53870592 11301 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13152 11301 603 41 0 13111 0 vsize: 52608 [startup+500.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11676 0 0 0 49964 41 0 0 25 0 1 0 481281060 54669312 11498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13347 11498 603 41 0 13306 0 vsize: 53388 [startup+510.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11848 0 0 0 50963 41 0 0 25 0 1 0 481281060 55341056 11670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13511 11670 603 41 0 13470 0 vsize: 54044 [startup+520.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 12052 0 0 0 51963 42 0 0 25 0 1 0 481281060 56143872 11874 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13707 11874 603 41 0 13666 0 vsize: 54828 [startup+530.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 12374 0 0 0 52963 42 0 0 25 0 1 0 481281060 57495552 12196 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14037 12196 603 41 0 13996 0 vsize: 56148 [startup+540.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 12871 0 0 0 53962 43 0 0 25 0 1 0 481281060 59510784 12693 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14529 12693 603 41 0 14488 0 vsize: 58116 [startup+550.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 13322 0 0 0 54962 44 0 0 25 0 1 0 481281060 61386752 13144 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14987 13144 603 41 0 14946 0 vsize: 59948 [startup+560.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 13984 0 0 0 55961 45 0 0 25 0 1 0 481281060 64049152 13806 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 13806 603 41 0 15596 0 vsize: 62548 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 14183 0 0 0 56961 45 0 0 25 0 1 0 481281060 64856064 14005 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15834 14005 603 41 0 15793 0 vsize: 63336 [startup+580.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 14363 0 0 0 57960 46 0 0 25 0 1 0 481281060 65662976 14185 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16031 14185 603 41 0 15990 0 vsize: 64124 [startup+590.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 14731 0 0 0 58960 47 0 0 25 0 1 0 481281060 67133440 14553 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16390 14553 603 41 0 16349 0 vsize: 65560 [startup+600.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15057 0 0 0 59959 47 0 0 25 0 1 0 481281060 68481024 14879 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16719 14879 603 41 0 16678 0 vsize: 66876 [startup+610.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28247 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 60958 48 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223844 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+620.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 61958 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+630.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 62959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+640.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 63959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+650.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 64959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+660.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 65959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+670.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 66959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+680.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 67959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+690.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 68960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+700.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 69960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+710.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 70960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+720.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 71960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+730.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 72960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+740.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 73960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+750.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 74961 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+760.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 75961 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17107 15274 603 41 0 17066 0 vsize: 68428 [startup+770.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 76961 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223616 1074718162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+780.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 77961 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+790.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 78961 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+800.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 79962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+810.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 80962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+820.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 81962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+830.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 82962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+840.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 83962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+850.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 84962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+860.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 85963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+870.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 86963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+880.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 87963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+890.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 88963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+900.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 89963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+910.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28249 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 90963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561278 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+920.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 91964 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+930.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 92964 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+940.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 93963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+950.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 94963 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+960.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 95963 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+970.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 96963 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+980.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 97964 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17105 15275 603 41 0 17064 0 vsize: 68420 [startup+990.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15626 0 0 0 98963 50 0 0 25 0 1 0 481281060 70733824 15448 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17269 15448 603 41 0 17228 0 vsize: 69076 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15806 0 0 0 99963 51 0 0 25 0 1 0 481281060 71544832 15628 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17467 15628 603 41 0 17426 0 vsize: 69868 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15941 0 0 0 100962 51 0 0 25 0 1 0 481281060 72077312 15763 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17597 15763 603 41 0 17556 0 vsize: 70388 [startup+1020.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16089 0 0 0 101962 52 0 0 25 0 1 0 481281060 72605696 15911 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17726 15911 603 41 0 17685 0 vsize: 70904 [startup+1030.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16241 0 0 0 102962 52 0 0 25 0 1 0 481281060 73273344 16063 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17889 16063 603 41 0 17848 0 vsize: 71556 [startup+1040.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16376 0 0 0 103962 52 0 0 25 0 1 0 481281060 73809920 16198 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18020 16198 603 41 0 17979 0 vsize: 72080 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16534 0 0 0 104962 53 0 0 25 0 1 0 481281060 74481664 16356 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18184 16356 603 41 0 18143 0 vsize: 72736 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16714 0 0 0 105961 53 0 0 25 0 1 0 481281060 75149312 16536 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18347 16536 603 41 0 18306 0 vsize: 73388 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16975 0 0 0 106960 55 0 0 25 0 1 0 481281060 76214272 16797 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18607 16797 603 41 0 18566 0 vsize: 74428 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 17267 0 0 0 107960 55 0 0 25 0 1 0 481281060 77422592 17089 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18902 17089 603 41 0 18861 0 vsize: 75608 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 17664 0 0 0 108959 56 0 0 25 0 1 0 481281060 79040512 17486 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19297 17486 603 41 0 19256 0 vsize: 77188 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 17974 0 0 0 109958 57 0 0 25 0 1 0 481281060 80252928 17796 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19593 17796 603 41 0 19552 0 vsize: 78372 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 18323 0 0 0 110957 58 0 0 25 0 1 0 481281060 81711104 18145 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19949 18145 603 41 0 19908 0 vsize: 79796 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 18597 0 0 0 111957 59 0 0 25 0 1 0 481281060 82780160 18419 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20210 18419 603 41 0 20169 0 vsize: 80840 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 18910 0 0 0 112957 59 0 0 25 0 1 0 481281060 84119552 18732 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20537 18732 603 41 0 20496 0 vsize: 82148 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 19226 0 0 0 113956 60 0 0 25 0 1 0 481281060 85446656 19048 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20861 19048 603 41 0 20820 0 vsize: 83444 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 19576 0 0 0 114955 61 0 0 25 0 1 0 481281060 86777856 19398 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21186 19398 603 41 0 21145 0 vsize: 84744 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 19963 0 0 0 115955 62 0 0 25 0 1 0 481281060 88371200 19785 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21575 19785 603 41 0 21534 0 vsize: 86300 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 20359 0 0 0 116954 63 0 0 25 0 1 0 481281060 89968640 20181 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21965 20181 603 41 0 21924 0 vsize: 87860 [startup+1180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 20706 0 0 0 117953 64 0 0 25 0 1 0 481281060 91439104 20528 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22324 20528 603 41 0 22283 0 vsize: 89296 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 21081 0 0 0 118952 65 0 0 25 0 1 0 481281060 92909568 20903 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22683 20903 603 41 0 22642 0 vsize: 90732 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28251 Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 21500 0 0 0 119951 66 0 0 25 0 1 0 481281060 94654464 21322 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23109 21322 603 41 0 23068 0 vsize: 92436 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 1/55 28251 Raw data (stat): 28243 (minisat+) Z 28242 20838 20837 0 -1 12 21503 0 0 0 119951 70 0 0 25 0 1 0 481281060 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.06 CPU time (s): 1200.23 CPU user time (s): 1199.52 CPU system time (s): 0.707892 CPU usage (%): 100.014 Max. virtual memory (Kb): 92436 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####