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 wulflinc24 THE 2005-04-13 21:58:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3335 boxname=wulflinc24 idbench=371 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: a89f4ed95903fddf213992506514bcf0 /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:98.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:98.opb IDLAUNCH: 3335 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 853116 kB Buffers: 33824 kB Cached: 105488 kB SwapCached: 3828 kB Active: 48720 kB Inactive: 97248 kB HighTotal: 131008 kB HighFree: 23212 kB LowTotal: 903652 kB LowFree: 829904 kB SwapTotal: 2097892 kB SwapFree: 2094064 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 29924 kB Committed_AS: 63508 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 22:18:30 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 3335 7 1200.18 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]---> Adder-cost: 2188 maxlim: 461 bits: 10/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 26442 86478 | 8814 0 0 nan | 0.000 % | c | 100 | 26442 86478 | 9695 100 380 3.8 | 2.547 % | c | 250 | 26433 86447 | 10664 248 1059 4.3 | 2.560 % | c | 476 | 26433 86447 | 11731 474 2412 5.1 | 2.560 % | c ============================================================================== c [1mFound solution: 206[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2 maxlim: 1214 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 806 | 26471 86617 | 8823 804 4288 5.3 | 2.560 % | c ============================================================================== c [1mFound solution: 143[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1277 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 814 | 26480 86667 | 8826 812 4330 5.3 | 2.560 % | c | 914 | 26480 86667 | 9708 912 8172 9.0 | 2.738 % | c | 1064 | 26480 86667 | 10679 1062 8878 8.4 | 2.738 % | c | 1289 | 26480 86667 | 11747 1287 13915 10.8 | 2.738 % | c | 1626 | 26480 86667 | 12922 1624 15594 9.6 | 2.738 % | c | 2132 | 26480 86667 | 14214 2130 18615 8.7 | 2.738 % | c | 2892 | 26480 86667 | 15635 2890 40463 14.0 | 2.738 % | c | 4031 | 26480 86667 | 17199 4029 61525 15.3 | 2.738 % | c | 5740 | 26480 86667 | 18919 5738 145592 25.4 | 2.738 % | c | 8302 | 26480 86667 | 20811 8300 400387 48.2 | 2.738 % | c | 12147 | 26480 86667 | 22892 12145 750271 61.8 | 2.738 % | c ============================================================================== c [1mFound solution: 130[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1290 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14029 | 26485 86701 | 8828 14027 824966 58.8 | 2.738 % | c | 14129 | 26485 86701 | 9710 7114 431246 60.6 | 2.789 % | c | 14279 | 26485 86701 | 10681 7264 431919 59.5 | 2.789 % | c | 14505 | 26485 86701 | 11750 7490 433807 57.9 | 2.789 % | c | 14842 | 26485 86701 | 12925 7827 440942 56.3 | 2.789 % | c | 15349 | 26485 86701 | 14217 8334 463419 55.6 | 2.789 % | c | 16108 | 26485 86701 | 15639 9093 482022 53.0 | 2.789 % | c | 17247 | 26485 86701 | 17203 10232 538561 52.6 | 2.789 % | c | 18955 | 26485 86701 | 18923 11940 602513 50.5 | 2.789 % | c | 21519 | 26485 86701 | 20815 14504 833364 57.5 | 2.789 % | c ============================================================================== c [1mFound solution: 127[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1293 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23171 | 26489 86723 | 8829 16156 882076 54.6 | 2.789 % | c | 23272 | 26489 86723 | 9711 8179 357304 43.7 | 2.814 % | c | 23422 | 26489 86723 | 10683 8329 358840 43.1 | 2.814 % | c | 23647 | 26489 86723 | 11751 8554 363731 42.5 | 2.814 % | c | 23984 | 26489 86723 | 12926 8891 369197 41.5 | 2.814 % | c | 24490 | 26489 86723 | 14219 9397 396462 42.2 | 2.814 % | c | 25250 | 26489 86723 | 15641 10157 425636 41.9 | 2.814 % | c | 26389 | 26489 86723 | 17205 11296 470056 41.6 | 2.814 % | c | 28097 | 26489 86723 | 18925 13004 538210 41.4 | 2.814 % | c | 30662 | 26489 86723 | 20818 15569 771366 49.5 | 2.814 % | c | 34507 | 26489 86723 | 22900 19414 1108591 57.1 | 2.814 % | c | 40273 | 26489 86723 | 25190 25180 1530602 60.8 | 2.814 % | c ============================================================================== c [1mFound solution: 117[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1303 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47450 | 26491 86738 | 8830 18237 1218106 66.8 | 2.814 % | c | 47550 | 26491 86738 | 9713 4660 289106 62.0 | 2.839 % | c | 47700 | 26491 86738 | 10684 4810 290323 60.4 | 2.839 % | c | 47925 | 26491 86738 | 11752 5035 300392 59.7 | 2.839 % | c | 48262 | 26491 86738 | 12928 5372 302069 56.2 | 2.839 % | c | 48768 | 26491 86738 | 14220 5878 320891 54.6 | 2.839 % | c | 49527 | 26491 86738 | 15642 6637 330420 49.8 | 2.839 % | c | 50666 | 26491 86738 | 17207 7776 374858 48.2 | 2.839 % | c | 52374 | 26491 86738 | 18927 9484 530806 56.0 | 2.839 % | c | 54937 | 26491 86738 | 20820 12047 686209 57.0 | 2.839 % | c | 58782 | 26491 86738 | 22902 15892 975705 61.4 | 2.839 % | c ============================================================================== c [1mFound solution: 109[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1311 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 60887 | 26492 86744 | 8830 17997 1087821 60.4 | 2.839 % | c | 60987 | 26492 86744 | 9713 9099 440274 48.4 | 2.852 % | c | 61137 | 26492 86744 | 10684 9249 442243 47.8 | 2.852 % | c | 61363 | 26492 86744 | 11752 9475 447923 47.3 | 2.852 % | c | 61701 | 26492 86744 | 12928 9813 460334 46.9 | 2.852 % | c | 62209 | 26492 86744 | 14220 10321 482479 46.7 | 2.852 % | c | 62968 | 26492 86744 | 15642 11080 518644 46.8 | 2.852 % | c | 64109 | 26492 86744 | 17207 12221 575864 47.1 | 2.852 % | c | 65817 | 26492 86744 | 18927 13929 671448 48.2 | 2.852 % | c | 68380 | 26492 86744 | 20820 16492 791321 48.0 | 2.852 % | c | 72224 | 26492 86744 | 22902 20336 1038178 51.1 | 2.852 % | c | 77993 | 26492 86744 | 25193 26105 1602134 61.4 | 2.852 % | c | 86642 | 26492 86744 | 27712 21702 1613426 74.3 | 2.852 % | c ============================================================================== c [1mFound solution: 107[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1313 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90492 | 26493 86754 | 8831 25552 1851614 72.5 | 2.852 % | c | 90592 | 26493 86754 | 9714 6488 296083 45.6 | 2.865 % | c | 90742 | 26493 86754 | 10685 6638 298105 44.9 | 2.865 % | c | 90967 | 26493 86754 | 11754 6863 301577 43.9 | 2.865 % | c | 91304 | 26493 86754 | 12929 7200 303911 42.2 | 2.865 % | c | 91810 | 26493 86754 | 14222 7706 318504 41.3 | 2.865 % | c | 92569 | 26493 86754 | 15644 8465 366545 43.3 | 2.865 % | c | 93708 | 26493 86754 | 17209 9604 427191 44.5 | 2.865 % | c | 95418 | 26493 86754 | 18930 11314 506391 44.8 | 2.865 % | c | 97982 | 26493 86754 | 20823 13878 666721 48.0 | 2.865 % | c | 101827 | 26493 86754 | 22905 17723 1003862 56.6 | 2.865 % | c | 107595 | 26493 86754 | 25195 23491 1603772 68.3 | 2.865 % | c | 116244 | 26493 86754 | 27715 18209 2007969 110.3 | 2.865 % | c | 129219 | 26493 86754 | 30487 14477 1299051 89.7 | 2.865 % | c | 148680 | 26493 86754 | 33535 33938 3505926 103.3 | 2.865 % | c | 177873 | 26493 86754 | 36889 19569 1981304 101.2 | 2.865 % | c ============================================================================== c [1mFound solution: 106[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1314 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 203130 | 26495 86767 | 8831 17932 2342869 130.7 | 2.865 % | c | 203230 | 26495 86767 | 9714 9066 1059460 116.9 | 2.877 % | c | 203380 | 26495 86767 | 10685 9216 1060308 115.1 | 2.877 % | c | 203605 | 26495 86767 | 11754 9441 1061663 112.5 | 2.877 % | c | 203942 | 26495 86767 | 12929 9778 1064191 108.8 | 2.877 % | c | 204450 | 26495 86767 | 14222 10286 1076718 104.7 | 2.877 % | c | 205211 | 26495 86767 | 15644 11047 1099524 99.5 | 2.877 % | c | 206350 | 26495 86767 | 17209 12186 1151779 94.5 | 2.877 % | c | 208058 | 26495 86767 | 18930 13894 1290178 92.9 | 2.877 % | c | 210620 | 26495 86767 | 20823 16456 1424602 86.6 | 2.877 % | c | 214466 | 26495 86767 | 22905 20302 1945374 95.8 | 2.877 % | c | 220234 | 26495 86767 | 25195 13589 1290861 95.0 | 2.877 % | c | 228886 | 26495 86767 | 27715 22241 2221897 99.9 | 2.877 % | c | 241860 | 26495 86767 | 30487 16824 1624022 96.5 | 2.877 % | c | 261324 | 26495 86767 | 33535 18036 1297748 72.0 | 2.877 % | c | 290519 | 26495 86767 | 36889 27027 2715164 100.5 | 2.877 % | c | 334311 | 26495 86767 | 40578 18135 1843579 101.7 | 2.877 % | c | 399995 | 26495 86767 | 44636 25387 6045749 238.1 | 2.877 % | c ============================================================================== c [1mFound solution: 98[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1322 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 445674 | 26500 86799 | 8833 37759 6320294 167.4 | 2.877 % | c | 445774 | 26500 86799 | 9716 6732 774985 115.1 | 2.915 % | c | 445924 | 26500 86799 | 10687 6882 775935 112.7 | 2.915 % | c | 446151 | 26500 86799 | 11756 7109 777542 109.4 | 2.915 % | c | 446488 | 26500 86799 | 12932 7446 782594 105.1 | 2.915 % | c | 446994 | 26500 86799 | 14225 7952 795902 100.1 | 2.915 % | c | 447753 | 26500 86799 | 15648 8711 803084 92.2 | 2.915 % | c | 448892 | 26500 86799 | 17213 9850 821221 83.4 | 2.915 % | c | 450600 | 26500 86799 | 18934 11558 878453 76.0 | 2.915 % | c | 453165 | 26500 86799 | 20827 14123 1062292 75.2 | 2.915 % | c | 457009 | 26500 86799 | 22910 17967 1272621 70.8 | 2.915 % | c | 462775 | 26500 86799 | 25201 11982 661214 55.2 | 2.915 % | c | 471427 | 26500 86799 | 27721 20634 1378808 66.8 | 2.915 % | c | 484402 | 26500 86799 | 30493 14154 2586201 182.7 | 2.915 % | c | 503864 | 26500 86799 | 33543 33616 5188761 154.4 | 2.915 % | c | 533056 | 26500 86799 | 36897 18884 2969903 157.3 | 2.915 % | c | 576845 | 26500 86799 | 40587 35392 5877484 166.1 | 2.915 % | c | 642534 | 26500 86799 | 44646 42901 8342933 194.5 | 2.915 % | 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 -v236 v123 v720 -v627 v12#### 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.91 0.95 0.90 2/54 32094 Raw data (stat): 32094 (runsolver) R 32093 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479368619 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.93 0.95 0.90 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 2800 0 0 0 991 7 0 0 25 0 1 0 479368619 13037568 2652 4294967295 134512640 134672761 3221224624 3221138992 134592331 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3183 2652 603 41 0 3142 0 vsize: 12732 [startup+20.0002 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 2928 0 0 0 1990 7 0 0 25 0 1 0 479368619 13561856 2780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3311 2780 603 41 0 3270 0 vsize: 13244 [startup+30.0011 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3607 0 0 0 2987 10 0 0 25 0 1 0 479368619 16392192 3459 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4002 3459 603 41 0 3961 0 vsize: 16008 [startup+40.0008 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3844 0 0 0 3986 10 0 0 25 0 1 0 479368619 17334272 3696 4294967295 134512640 134672761 3221224624 3221223728 134555093 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4232 3696 603 41 0 4191 0 vsize: 16928 [startup+50.0012 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3844 0 0 0 4987 10 0 0 25 0 1 0 479368619 17334272 3696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4232 3696 603 41 0 4191 0 vsize: 16928 [startup+60.0012 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3844 0 0 0 5987 10 0 0 25 0 1 0 479368619 17334272 3696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4232 3696 603 41 0 4191 0 vsize: 16928 [startup+70.0009 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3905 0 0 0 6987 10 0 0 25 0 1 0 479368619 17604608 3757 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4298 3757 603 41 0 4257 0 vsize: 17192 [startup+80.0016 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 4158 0 0 0 7986 11 0 0 25 0 1 0 479368619 18616320 4010 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4545 4010 603 41 0 4504 0 vsize: 18180 [startup+90.0013 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 32094 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 4161 0 0 0 8986 11 0 0 25 0 1 0 479368619 18616320 4013 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4545 4013 603 41 0 4504 0 vsize: 18180 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.91 3/57 32133 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 4443 0 0 0 9986 12 0 0 25 0 1 0 479368619 19824640 4295 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4840 4295 603 41 0 4799 0 vsize: 19360 [startup+110.004 s] Raw data (loadavg): 1.06 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5412 0 0 0 10983 15 0 0 25 0 1 0 479368619 23732224 5264 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5794 5264 603 41 0 5753 0 vsize: 23176 [startup+120.003 s] Raw data (loadavg): 1.05 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5643 0 0 0 11983 15 0 0 25 0 1 0 479368619 24678400 5495 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6025 5495 603 41 0 5984 0 vsize: 24100 [startup+130.004 s] Raw data (loadavg): 1.04 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5643 0 0 0 12983 15 0 0 25 0 1 0 479368619 24678400 5495 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6025 5495 603 41 0 5984 0 vsize: 24100 [startup+140.004 s] Raw data (loadavg): 1.03 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5807 0 0 0 13983 16 0 0 25 0 1 0 479368619 25477120 5659 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6220 5659 603 41 0 6179 0 vsize: 24880 [startup+150.005 s] Raw data (loadavg): 1.03 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5963 0 0 0 14983 16 0 0 25 0 1 0 479368619 26148864 5815 4294967295 134512640 134672761 3221224624 3221223856 134541816 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6384 5815 603 41 0 6343 0 vsize: 25536 [startup+160.004 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5963 0 0 0 15983 16 0 0 25 0 1 0 479368619 26148864 5815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6384 5815 603 41 0 6343 0 vsize: 25536 [startup+170.004 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 32147 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6289 0 0 0 16983 17 0 0 25 0 1 0 479368619 27496448 6141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6713 6141 603 41 0 6672 0 vsize: 26852 [startup+180.004 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6505 0 0 0 17982 18 0 0 25 0 1 0 479368619 28438528 6357 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6943 6357 603 41 0 6902 0 vsize: 27772 [startup+190.004 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6505 0 0 0 18982 18 0 0 25 0 1 0 479368619 28438528 6357 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6943 6357 603 41 0 6902 0 vsize: 27772 [startup+200.005 s] Raw data (loadavg): 1.08 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6505 0 0 0 19982 18 0 0 25 0 1 0 479368619 28438528 6357 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6943 6357 603 41 0 6902 0 vsize: 27772 [startup+210.005 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6993 0 0 0 20981 19 0 0 25 0 1 0 479368619 30449664 6845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7434 6845 603 41 0 7393 0 vsize: 29736 [startup+220.005 s] Raw data (loadavg): 1.05 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7952 0 0 0 21979 22 0 0 25 0 1 0 479368619 34336768 7804 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8383 7804 603 41 0 8342 0 vsize: 33532 [startup+230.005 s] Raw data (loadavg): 1.05 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 22979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8416 7839 603 41 0 8375 0 vsize: 33664 [startup+240.005 s] Raw data (loadavg): 1.04 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 23979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8416 7839 603 41 0 8375 0 vsize: 33664 [startup+250.006 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 24979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8416 7839 603 41 0 8375 0 vsize: 33664 [startup+260.005 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 25979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8416 7839 603 41 0 8375 0 vsize: 33664 [startup+270.005 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 26979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8416 7839 603 41 0 8375 0 vsize: 33664 [startup+280.006 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 27980 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223580 1075349771 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8416 7839 603 41 0 8375 0 vsize: 33664 [startup+290.006 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 28980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+300.006 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 29980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+310.007 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 30980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+320.007 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 31980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+330.007 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 32981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+340.007 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 33981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+350.008 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 34981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+360.009 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 35981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+370.008 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 36981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+380.008 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 37982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+390.008 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 38982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+400.009 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 39982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+410.009 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 40982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8414 7839 603 41 0 8373 0 vsize: 33656 [startup+420.009 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 8142 0 0 0 41982 23 0 0 25 0 1 0 479368619 35139584 7994 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8579 7994 603 41 0 8538 0 vsize: 34316 [startup+430.009 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9009 0 0 0 42980 25 0 0 25 0 1 0 479368619 38637568 8861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9433 8861 603 41 0 9392 0 vsize: 37732 [startup+440.009 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 43979 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9564 8998 603 41 0 9523 0 vsize: 38256 [startup+450.01 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 44980 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9564 8998 603 41 0 9523 0 vsize: 38256 [startup+460.01 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 45980 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9564 8998 603 41 0 9523 0 vsize: 38256 [startup+470.01 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32149 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 46980 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223728 134560070 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9564 8998 603 41 0 9523 0 vsize: 38256 [startup+480.01 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9922 0 0 0 47978 27 0 0 25 0 1 0 479368619 42401792 9774 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10352 9774 603 41 0 10311 0 vsize: 41408 [startup+490.01 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 10612 0 0 0 48977 29 0 0 25 0 1 0 479368619 45252608 10464 4294967295 134512640 134672761 3221224624 3221223728 134554926 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11048 10464 603 41 0 11007 0 vsize: 44192 [startup+500.011 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 11365 0 0 0 49975 31 0 0 25 0 1 0 479368619 48349184 11217 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11804 11217 603 41 0 11763 0 vsize: 47216 [startup+510.011 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 12060 0 0 0 50973 33 0 0 25 0 1 0 479368619 51175424 11912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12494 11912 603 41 0 12453 0 vsize: 49976 [startup+520.01 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 12810 0 0 0 51971 36 0 0 25 0 1 0 479368619 54272000 12662 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13250 12662 603 41 0 13209 0 vsize: 53000 [startup+530.011 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 52968 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+540.011 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 53969 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+550.012 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 54969 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+560.012 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 55969 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+570.012 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 56968 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+580.013 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 57968 39 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+590.013 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 58968 39 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13809 13212 603 41 0 13768 0 vsize: 55236 [startup+600.015 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13362 0 0 0 59968 39 0 0 25 0 1 0 479368619 56561664 13214 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13809 13214 603 41 0 13768 0 vsize: 55236 [startup+610.015 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 60968 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13791 13215 603 41 0 13750 0 vsize: 55164 [startup+620.014 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 61967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13791 13215 603 41 0 13750 0 vsize: 55164 [startup+630.015 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 62967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13791 13215 603 41 0 13750 0 vsize: 55164 [startup+640.015 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 63967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13791 13215 603 41 0 13750 0 vsize: 55164 [startup+650.015 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 64967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13791 13215 603 41 0 13750 0 vsize: 55164 [startup+660.017 s] Raw data (loadavg): 1.00 1.00 0.92 3/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 65967 41 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13707 13146 603 41 0 13666 0 vsize: 54828 [startup+670.017 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 66966 41 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13707 13146 603 41 0 13666 0 vsize: 54828 [startup+680.018 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 67966 42 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13707 13146 603 41 0 13666 0 vsize: 54828 [startup+690.019 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 68966 42 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13707 13146 603 41 0 13666 0 vsize: 54828 [startup+700.019 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 69966 43 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223624 1075350113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+710.02 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 70966 43 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+720.02 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 71965 43 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+730.021 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 72965 44 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+740.022 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 73965 44 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+750.023 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 74965 45 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+760.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 75965 45 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13696 13135 603 41 0 13655 0 vsize: 54784 [startup+770.023 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 76964 45 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+780.023 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 77963 46 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+790.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 78963 46 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+800.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 79963 47 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+810.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 80963 47 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223804 134559056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+820.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 81962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+830.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 82962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+840.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 83962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223720 1075347361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+850.025 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 84962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+860.025 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 85961 49 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+870.025 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 86961 49 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+880.026 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 87960 50 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+890.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 88960 50 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223564 1075350563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+900.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 89960 51 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+910.028 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 90959 51 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+920.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 91959 52 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+930.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 92959 52 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+940.028 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 93959 52 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+950.028 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 94958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+960.029 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 95958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223808 134559625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+970.029 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 96958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223804 134559056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+980.029 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 97958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+990.029 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 98958 54 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1000.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 99958 54 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1010.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 100957 54 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1020.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 101957 55 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1030.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 102957 55 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1040.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 103957 55 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1050.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 104957 56 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1060.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 105956 56 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1070.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 106956 57 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1080.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 107956 57 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13075 603 41 0 13595 0 vsize: 54544 [startup+1090.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 108955 57 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1100.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 109955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1110.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 110955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1120.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 111955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1130.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 112955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1140.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 113955 59 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1150.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 114955 59 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1160.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 115954 59 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1170.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 116954 60 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13636 13077 603 41 0 13595 0 vsize: 54544 [startup+1180.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13367 0 0 0 117954 60 0 0 25 0 1 0 479368619 55853056 13078 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13636 13078 603 41 0 13595 0 vsize: 54544 [startup+1190.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13367 0 0 0 118955 60 0 0 25 0 1 0 479368619 55853056 13078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13636 13078 603 41 0 13595 0 vsize: 54544 [startup+1200.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 32151 Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13367 0 0 0 119955 60 0 0 25 0 1 0 479368619 55853056 13078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13636 13078 603 41 0 13595 0 vsize: 54544 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 1.00 1.00 0.92 1/54 32151 Raw data (stat): 32094 (minisat+) Z 32093 28546 28545 0 -1 12 13370 0 0 0 119955 62 0 0 25 0 1 0 479368619 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.07 CPU time (s): 1200.18 CPU user time (s): 1199.56 CPU system time (s): 0.624905 CPU usage (%): 100.009 Max. virtual memory (Kb): 55236 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####