Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb |
MD5SUM | 46c4db5f8baf54496e00a723c85beb20 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 58880896 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1095 |
Biggest coefficient in the objective function | 533200896 |
Number of bits for the biggest coefficient in the objective function | 29 |
Sum of the numbers in the objective function | 14929722305 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 533200896 |
Number of bits of the biggest number in a constraint | 29 |
Biggest sum of numbers in a constraint | 14929722305 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04084 |
Number of variables | 1155 |
Total number of constraints | 153 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 55 |
Number of constraints which are nor clauses,nor cardinality constraints | 98 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 280 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-05-27 08:45:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23648 boxname=wulflinc19 idbench=1292 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 46c4db5f8baf54496e00a723c85beb20 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-egout.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 23648 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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.037 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: 895784 kB Buffers: 1852 kB Cached: 116448 kB SwapCached: 700 kB Active: 14532 kB Inactive: 105988 kB HighTotal: 131008 kB HighFree: 11564 kB LowTotal: 903652 kB LowFree: 884220 kB SwapTotal: 2097892 kB SwapFree: 2096396 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5196 kB Slab: 12636 kB Committed_AS: 63564 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 09:06:24 (client local time) WITH STATUS 152 IN 1229.88 SECONDS stats: 23648 7 1229.88 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 115 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ########################### c -- Clauses(.)/Splits(s): (none) c ---[ 113]---> BDD-cost: 2069 c ---[ 111]---> BDD-cost: 40 c ---[ 109]---> BDD-cost: 25 c ---[ 107]---> BDD-cost: 45 c ---[ 105]---> BDD-cost: 83 c ---[ 101]---> BDD-cost: 39 c ---[ 99]---> BDD-cost: 100 c ---[ 97]---> BDD-cost: 34 c ---[ 91]---> BDD-cost: 55 c ---[ 89]---> BDD-cost: 40 c ---[ 85]---> BDD-cost: 128 c ---[ 83]---> BDD-cost: 40 c ---[ 81]---> BDD-cost: 112 c ---[ 79]---> BDD-cost: 49 c ---[ 75]---> BDD-cost: 45 c ---[ 73]---> BDD-cost: 28 c ---[ 71]---> BDD-cost: 214 c ---[ 69]---> BDD-cost: 55 c ---[ 67]---> BDD-cost: 123 c ---[ 65]---> BDD-cost: 118 c ---[ 59]---> BDD-cost: 51 c ---[ 57]---> BDD-cost: 40 c ---[ 55]---> BDD-cost: 40 c ---[ 53]---> BDD-cost: 51 c ---[ 49]---> BDD-cost: 135 c ---[ 47]---> BDD-cost: 135 c ---[ 45]---> BDD-cost: 49 c ---[ 44]---> BDD-cost: 9 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 9 c ---[ 41]---> BDD-cost: 10 c ---[ 40]---> BDD-cost: 10 c ---[ 39]---> BDD-cost: 11 c ---[ 37]---> BDD-cost: 12 c ---[ 36]---> BDD-cost: 12 c ---[ 35]---> BDD-cost: 12 c ---[ 34]---> BDD-cost: 12 c ---[ 31]---> BDD-cost: 12 c ---[ 30]---> BDD-cost: 12 c ---[ 29]---> BDD-cost: 13 c ---[ 27]---> BDD-cost: 26 c ---[ 26]---> BDD-cost: 26 c ---[ 25]---> BDD-cost: 26 c ---[ 24]---> BDD-cost: 26 c ---[ 23]---> BDD-cost: 26 c ---[ 21]---> BDD-cost: 10 c ---[ 20]---> BDD-cost: 10 c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 26 c ---[ 17]---> BDD-cost: 26 c ---[ 16]---> BDD-cost: 12 c ---[ 15]---> BDD-cost: 12 c ---[ 14]---> BDD-cost: 26 c ---[ 13]---> BDD-cost: 26 c ---[ 12]---> BDD-cost: 26 c ---[ 9]---> BDD-cost: 26 c ---[ 8]---> BDD-cost: 26 c ---[ 7]---> BDD-cost: 26 c ---[ 6]---> BDD-cost: 26 c ---[ 4]---> BDD-cost: 26 c ---[ 3]---> BDD-cost: 26 c ---[ 2]---> BDD-cost: 26 c ---[ 1]---> BDD-cost: 26 c ---[ 0]---> BDD-cost: 26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11251 30877 | 3750 0 0 nan | 0.000 % | c | 100 | 11251 30877 | 4125 100 1515 15.2 | 13.712 % | c | 250 | 11125 30605 | 4537 201 3790 18.9 | 14.852 % | c ============================================================================== c [1mFound solution: 104597997[0m c ---[ 0]---> Sorter-cost:93787 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 312 | 275979 648913 | 91993 258 4502 17.4 | 14.852 % | c | 414 | 275839 648590 | 101192 359 5633 15.7 | 0.876 % | c | 566 | 273633 643567 | 111311 491 6737 13.7 | 1.527 % | c | 791 | 272629 641263 | 122442 694 11999 17.3 | 1.833 % | c | 1129 | 272332 640587 | 134686 1031 13927 13.5 | 1.923 % | c | 1637 | 269162 633419 | 148155 1521 18036 11.9 | 2.840 % | c | 2401 | 269146 633387 | 162971 2277 24619 10.8 | 2.849 % | c ============================================================================== c [1mFound solution: 103969862[0m c ---[ 0]---> Sorter-cost:62175 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2789 | 442636 1038731 | 147545 2648 27001 10.2 | 2.849 % | c | 2890 | 442630 1038719 | 162299 2746 28785 10.5 | 1.843 % | c | 3040 | 442133 1037580 | 178529 2873 30427 10.6 | 1.941 % | c | 3265 | 442133 1037580 | 196382 3098 33041 10.7 | 1.941 % | c | 3602 | 442099 1037510 | 216020 3421 35738 10.4 | 1.950 % | c ============================================================================== c [1mFound solution: 101568271[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3651 | 442571 1039056 | 147523 3469 36095 10.4 | 1.950 % | c | 3751 | 440803 1035063 | 162275 3568 36923 10.3 | 2.270 % | c | 3901 | 440803 1035063 | 178502 3718 37747 10.2 | 2.270 % | c | 4126 | 440579 1034544 | 196353 3940 39603 10.1 | 2.317 % | c | 4463 | 438220 1029144 | 215988 4267 46139 10.8 | 2.777 % | c ============================================================================== c [1mFound solution: 100803003[0m c ---[ 0]---> Sorter-cost:55983 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4817 | 593599 1391936 | 197866 4598 51840 11.3 | 2.777 % | c | 4917 | 593599 1391936 | 217652 4698 53220 11.3 | 2.178 % | c | 5068 | 593599 1391936 | 239417 4849 64015 13.2 | 2.178 % | c | 5294 | 593583 1391900 | 263359 5073 65615 12.9 | 2.180 % | c ============================================================================== c [1mFound solution: 100684650[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5609 | 594151 1393683 | 198050 5387 69571 12.9 | 2.180 % | c | 5709 | 594151 1393683 | 217855 5487 72393 13.2 | 2.178 % | c | 5859 | 593587 1392402 | 239640 5633 73644 13.1 | 2.255 % | c | 6084 | 592959 1390991 | 263604 5855 75225 12.8 | 2.341 % | c ============================================================================== c [1mFound solution: 92797205[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6220 | 593520 1392339 | 197840 5991 77445 12.9 | 2.341 % | c | 6320 | 593520 1392339 | 217624 6091 79073 13.0 | 2.338 % | c | 6470 | 591484 1387732 | 239386 6216 80899 13.0 | 2.618 % | c | 6696 | 591484 1387732 | 263325 6442 83338 12.9 | 2.618 % | c ============================================================================== c [1mFound solution: 83460735[0m c ---[ 0]---> Sorter-cost:45803 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6906 | 715900 1678230 | 238633 6632 89539 13.5 | 2.618 % | c | 7007 | 715884 1678194 | 262496 6732 92667 13.8 | 2.314 % | c | 7157 | 715884 1678194 | 288745 6882 105493 15.3 | 2.314 % | c | 7382 | 715685 1677751 | 317620 7102 134992 19.0 | 2.338 % | c | 7720 | 715422 1677166 | 349382 7431 137680 18.5 | 2.368 % | c | 8226 | 714699 1675530 | 384320 7925 140440 17.7 | 2.452 % | c ============================================================================== c [1mFound solution: 77397424[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8562 | 715491 1677827 | 238497 8258 144917 17.5 | 2.452 % | c | 8664 | 715379 1677582 | 262346 8356 145663 17.4 | 2.483 % | c | 8814 | 715364 1677550 | 288581 8505 146796 17.3 | 2.485 % | c | 9039 | 714976 1676674 | 317439 8719 151496 17.4 | 2.532 % | c | 9379 | 712783 1671706 | 349183 9013 167373 18.6 | 2.788 % | c | 9885 | 712783 1671706 | 384101 9519 195590 20.5 | 2.788 % | c ============================================================================== c [1mFound solution: 75180416[0m c ---[ 0]---> Sorter-cost:37038 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10054 | 811550 1902194 | 270516 9688 208790 21.6 | 2.788 % | c ============================================================================== c [1mFound solution: 73788603[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10119 | 812452 1904799 | 270817 9753 216393 22.2 | 2.788 % | c | 10219 | 811528 1902727 | 297898 9844 216942 22.0 | 2.723 % | c | 10369 | 810256 1899884 | 327688 9969 219537 22.0 | 2.845 % | c | 10594 | 810078 1899482 | 360457 10187 229042 22.5 | 2.862 % | c | 10934 | 809700 1898635 | 396503 10525 232743 22.1 | 2.897 % | c | 11440 | 809688 1898608 | 436153 11030 269210 24.4 | 2.899 % | c ============================================================================== c [1mFound solution: 70890816[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11567 | 808629 1896282 | 269543 11141 294797 26.5 | 2.899 % | c | 11667 | 808538 1896075 | 296497 11239 295298 26.3 | 3.045 % | c | 11820 | 808382 1895723 | 326147 11391 296270 26.0 | 3.061 % | c | 12045 | 808374 1895705 | 358761 11615 335819 28.9 | 3.062 % | c | 12383 | 807678 1894121 | 394637 11942 344697 28.9 | 3.132 % | c ============================================================================== c [1mFound solution: 70763968[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12669 | 807537 1893992 | 269179 12225 349850 28.6 | 3.132 % | c | 12769 | 807487 1893881 | 296096 12324 351330 28.5 | 3.154 % | c ============================================================================== c [1mFound solution: 70626176[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12794 | 807503 1893991 | 269167 12349 353606 28.6 | 3.154 % | c | 12896 | 807503 1893991 | 296083 12451 356275 28.6 | 3.154 % | c ============================================================================== c [1mFound solution: 70027776[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12938 | 807532 1894068 | 269177 12493 356758 28.6 | 3.154 % | c ============================================================================== c [1mFound solution: 70025856[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12974 | 807548 1894113 | 269182 12529 360715 28.8 | 3.154 % | c | 13075 | 807135 1893185 | 296100 12589 361725 28.7 | 3.201 % | c | 13225 | 807110 1893129 | 325710 12738 368507 28.9 | 3.204 % | c ============================================================================== c [1mFound solution: 68001664[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13371 | 807126 1893171 | 269042 12884 380444 29.5 | 3.204 % | c | 13471 | 807077 1893059 | 295946 12981 380994 29.4 | 3.209 % | c | 13621 | 807044 1892982 | 325540 13130 382392 29.1 | 3.214 % | c | 13846 | 807044 1892982 | 358094 13355 383733 28.7 | 3.214 % | c ============================================================================== c [1mFound solution: 65174016[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13997 | 807035 1892975 | 269011 13505 388162 28.7 | 3.214 % | c ============================================================================== c [1mFound solution: 62291456[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14037 | 807058 1893037 | 269019 13545 388559 28.7 | 3.214 % | c | 14137 | 807049 1893018 | 295920 13605 389920 28.7 | 3.222 % | c | 14287 | 807049 1893018 | 325512 13755 392019 28.5 | 3.222 % | c | 14512 | 807049 1893018 | 358064 13980 397143 28.4 | 3.222 % | c | 14851 | 807049 1893018 | 393870 14319 417509 29.2 | 3.222 % | c ============================================================================== c [1mFound solution: 62282321[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15069 | 807074 1893084 | 269024 14537 424496 29.2 | 3.222 % | c ============================================================================== c [1mFound solution: 62280682[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15106 | 807085 1893117 | 269028 14574 433145 29.7 | 3.222 % | c | 15207 | 807085 1893117 | 295930 14675 436853 29.8 | 3.223 % | c | 15358 | 807064 1893070 | 325523 14824 442215 29.8 | 3.225 % | c | 15583 | 807064 1893070 | 358076 15049 447226 29.7 | 3.225 % | c | 15920 | 807064 1893070 | 393883 15386 453459 29.5 | 3.225 % | c | 16426 | 807064 1893070 | 433272 15892 469778 29.6 | 3.225 % | c ============================================================================== c [1mFound solution: 62227456[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16835 | 807075 1893101 | 269025 16301 485940 29.8 | 3.225 % | c | 16939 | 807075 1893101 | 295927 16405 488704 29.8 | 3.226 % | c | 17089 | 807075 1893101 | 325520 16555 492833 29.8 | 3.226 % | c | 17314 | 807075 1893101 | 358072 16780 500117 29.8 | 3.226 % | c | 17651 | 807075 1893101 | 393879 17117 513203 30.0 | 3.226 % | c | 18157 | 807075 1893101 | 433267 17623 525729 29.8 | 3.226 % | c | 18916 | 806798 1892471 | 476594 17898 539622 30.1 | 3.261 % | c ============================================================================== c [1mFound solution: 62187392[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19541 | 806810 1892502 | 268936 18523 588761 31.8 | 3.261 % | c | 19642 | 806810 1892502 | 295829 18624 596304 32.0 | 3.261 % | c | 19792 | 806810 1892502 | 325412 18774 601693 32.0 | 3.261 % | c ============================================================================== c [1mFound solution: 62183922[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19829 | 806828 1892551 | 268942 18811 603364 32.1 | 3.261 % | c ============================================================================== c [1mFound solution: 62094660[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19849 | 806849 1892602 | 268949 18831 605524 32.2 | 3.261 % | c ============================================================================== c [1mFound solution: 62092608[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19920 | 806861 1892632 | 268953 18902 607820 32.2 | 3.261 % | c ============================================================================== c [1mFound solution: 62091582[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19938 | 806885 1892690 | 268961 18920 609878 32.2 | 3.261 % | c ============================================================================== c [1mFound solution: 62076192[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19949 | 806903 1892732 | 268967 18931 611632 32.3 | 3.261 % | c ============================================================================== c [1mFound solution: 62063880[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19953 | 806917 1892772 | 268972 18935 611739 32.3 | 3.261 % | c ============================================================================== c [1mFound solution: 62060802[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19955 | 806934 1892819 | 268978 18937 612184 32.3 | 3.261 % | c ============================================================================== c [1mFound solution: 62048640[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19964 | 806947 1892853 | 268982 18946 613024 32.4 | 3.261 % | c ============================================================================== c [1mFound solution: 61994112[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19984 | 806963 1892892 | 268987 18966 613589 32.4 | 3.261 % | c | 20085 | 806963 1892892 | 295885 19067 618175 32.4 | 3.263 % | c | 20239 | 806963 1892892 | 325474 19221 629026 32.7 | 3.263 % | c | 20464 | 806963 1892892 | 358021 19446 637755 32.8 | 3.263 % | c | 20801 | 806963 1892892 | 393823 19783 655589 33.1 | 3.263 % | c | 21308 | 806963 1892892 | 433206 20290 688527 33.9 | 3.263 % | c | 22067 | 806963 1892892 | 476526 21049 718717 34.1 | 3.263 % | c ============================================================================== c [1mFound solution: 61947942[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22419 | 806856 1892653 | 268952 21400 735156 34.4 | 3.263 % | c | 22519 | 806856 1892653 | 295847 21500 736809 34.3 | 3.275 % | c ============================================================================== c [1mFound solution: 61892736[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22581 | 806871 1892688 | 268957 21562 739420 34.3 | 3.275 % | c ============================================================================== c [1mFound solution: 61163008[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22624 | 806889 1892730 | 268963 21605 745725 34.5 | 3.275 % | c | 22725 | 806889 1892730 | 295859 21706 752916 34.7 | 3.276 % | c | 22877 | 806889 1892730 | 325445 21858 760442 34.8 | 3.276 % | c | 23102 | 806889 1892730 | 357989 22083 767078 34.7 | 3.276 % | c | 23439 | 806889 1892730 | 393788 22420 780500 34.8 | 3.276 % | c | 23950 | 806889 1892730 | 433167 22931 812292 35.4 | 3.276 % | c | 24709 | 806889 1892730 | 476484 23690 835996 35.3 | 3.276 % | c | 25848 | 806889 1892730 | 524132 24829 896161 36.1 | 3.276 % | c ============================================================================== c [1mFound solution: 61074176[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26578 | 806893 1892748 | 268964 25558 923539 36.1 | 3.276 % | c | 26681 | 806893 1892748 | 295860 25661 929030 36.2 | 3.278 % | c | 26833 | 806893 1892748 | 325446 25813 934761 36.2 | 3.278 % | c | 27059 | 806893 1892748 | 357991 26039 948932 36.4 | 3.278 % | c | 27397 | 806893 1892748 | 393790 26377 962574 36.5 | 3.278 % | c | 27903 | 806893 1892748 | 433169 26883 982580 36.6 | 3.278 % | c | 28662 | 806893 1892748 | 476486 27642 1038039 37.6 | 3.278 % | c | 29803 | 806893 1892748 | 524134 28783 1085148 37.7 | 3.278 % | c | 31511 | 806893 1892748 | 576548 30491 1158917 38.0 | 3.278 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 3548 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.78 0.92 0.90 1/54 3544 Raw data (stat): 3544 (runsolver) D 3543 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 854819979 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.82 0.93 0.90 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0016 s] Raw data (loadavg): 0.84 0.93 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0018 s] Raw data (loadavg): 0.87 0.93 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0022 s] Raw data (loadavg): 0.89 0.93 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0019 s] Raw data (loadavg): 0.90 0.93 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0024 s] Raw data (loadavg): 0.92 0.93 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0026 s] Raw data (loadavg): 0.93 0.94 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0024 s] Raw data (loadavg): 0.94 0.94 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0022 s] Raw data (loadavg): 0.95 0.94 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.002 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.97 0.94 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.003 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3548 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.026 s] Raw data (loadavg): 0.99 0.97 0.91 3/58 3571 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.028 s] Raw data (loadavg): 1.14 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.028 s] Raw data (loadavg): 1.12 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.027 s] Raw data (loadavg): 1.10 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.028 s] Raw data (loadavg): 1.08 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.028 s] Raw data (loadavg): 1.07 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.029 s] Raw data (loadavg): 1.06 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.03 s] Raw data (loadavg): 1.05 1.00 0.92 2/55 3601 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.029 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.03 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.03 s] Raw data (loadavg): 1.03 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.031 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.032 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.031 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.032 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.03 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.03 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.03 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.03 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.03 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3603 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.73 s] Raw data (loadavg): 1.00 1.00 0.92 1/53 3605 Raw data (stat): 3544 (minisat+_script) S 3543 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819979 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.73 CPU time (s): 1229.88 CPU user time (s): 1229.06 CPU system time (s): 0.825874 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####