Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0291.opb |
MD5SUM | 1d9168a9335e29df835d07b0bdf2adea |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 10447498 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 289 |
Biggest coefficient in the objective function | 80000000 |
Number of bits for the biggest coefficient in the objective function | 27 |
Sum of the numbers in the objective function | 686518451 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 80000000 |
Number of bits of the biggest number in a constraint | 27 |
Biggest sum of numbers in a constraint | 686518451 |
Number of bits of the biggest sum of numbers | 30 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.335948 |
Number of variables | 291 |
Total number of constraints | 543 |
Number of constraints which are clauses | 189 |
Number of constraints which are cardinality constraints (but not clauses) | 295 |
Number of constraints which are nor clauses,nor cardinality constraints | 59 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 53 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-21 09:09:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12152 boxname=wulflinc7 idbench=935 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1d9168a9335e29df835d07b0bdf2adea /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-p0291.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-p0291.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-p0291.opb IDLAUNCH: 12152 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 2 cpu MHz : 451.050 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: 694992 kB Buffers: 19592 kB Cached: 297896 kB SwapCached: 4 kB Active: 72564 kB Inactive: 247768 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 694740 kB SwapTotal: 2097136 kB SwapFree: 2097132 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6940 kB Slab: 13592 kB Committed_AS: 63560 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 09:29:03 (client local time) WITH STATUS 10 IN 1200.17 SECONDS stats: 12152 7 1200.17 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 205 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss c ---[ 144]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 139]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 14]---> Adder-cost: 147 maxlim: 485 bits: 10/9 c ---[ 13]---> Adder-cost: 117 maxlim: 539 bits: 11/10 c ---[ 11]---> Adder-cost: 104 maxlim: 51 bits: 7/6 c ---[ 10]---> Adder-cost: 104 maxlim: 51 bits: 7/6 c ---[ 9]---> Adder-cost: 104 maxlim: 51 bits: 7/6 c ---[ 8]---> Adder-cost: 24 maxlim: 11 bits: 5/4 c ---[ 7]---> Adder-cost: 15 maxlim: 7 bits: 4/3 c ---[ 6]---> Adder-cost: 31 maxlim: 15 bits: 5/4 c ---[ 5]---> Adder-cost: 56 maxlim: 27 bits: 6/5 c ---[ 4]---> Adder-cost: 24 maxlim: 19 bits: 6/5 c ---[ 3]---> Adder-cost: 59 maxlim: 55 bits: 7/6 c ---[ 2]---> Adder-cost: 81 maxlim: 87 bits: 8/7 c ---[ 1]---> Adder-cost: 91 maxlim: 159 bits: 9/8 c ---[ 0]---> Adder-cost: 18 maxlim: 19 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 6296 22114 | 2098 0 0 nan | 0.000 % | c | 100 | 6296 22114 | 2307 100 557 5.6 | 3.157 % | c | 251 | 6296 22114 | 2538 251 1772 7.1 | 3.157 % | c ============================================================================== c [1mFound solution: 52128157[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 4008 maxlim: 424299904 bits: 29/29 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 471 | 34009 121116 | 11336 470 3736 7.9 | 3.157 % | c | 571 | 34009 121116 | 12469 570 4461 7.8 | 1.154 % | c | 721 | 33984 121033 | 13716 715 5649 7.9 | 1.230 % | c | 946 | 33926 120831 | 15088 925 7236 7.8 | 1.381 % | c | 1284 | 33918 120805 | 16597 1261 11375 9.0 | 1.419 % | c | 1793 | 33918 120805 | 18256 1770 16948 9.6 | 1.419 % | c | 2552 | 33918 120805 | 20082 2529 30167 11.9 | 1.419 % | c | 3691 | 33918 120805 | 22090 3668 54647 14.9 | 1.419 % | c | 5400 | 33909 120774 | 24299 5376 90480 16.8 | 1.438 % | c | 7966 | 33909 120774 | 26729 7942 166044 20.9 | 1.438 % | c | 11810 | 33909 120774 | 29402 11786 328844 27.9 | 1.438 % | c | 17576 | 33909 120774 | 32342 17552 587265 33.5 | 1.438 % | c | 26226 | 33882 120677 | 35577 26200 991686 37.9 | 1.457 % | c | 39200 | 33882 120677 | 39134 39174 2081877 53.1 | 1.457 % | c | 58662 | 33861 120602 | 43048 32882 2757349 83.9 | 1.476 % | c | 87854 | 33861 120602 | 47353 31925 2294066 71.9 | 1.476 % | c ============================================================================== c [1mFound solution: 51953164[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2666 maxlim: 386959717 bits: 29/29 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 95344 | 52322 186563 | 17440 39413 2669923 67.7 | 1.476 % | c | 95446 | 52322 186563 | 19184 15184 805936 53.1 | 1.155 % | c | 95596 | 52322 186563 | 21102 15334 806853 52.6 | 1.155 % | c | 95821 | 52322 186563 | 23212 15559 812645 52.2 | 1.155 % | c | 96161 | 52322 186563 | 25533 15899 821655 51.7 | 1.156 % | c | 96668 | 52322 186563 | 28087 16406 833043 50.8 | 1.155 % | c | 97427 | 52322 186563 | 30896 17165 870249 50.7 | 1.155 % | c | 98566 | 52322 186563 | 33985 18304 919224 50.2 | 1.155 % | c | 100275 | 52322 186563 | 37384 20013 969974 48.5 | 1.155 % | c | 102837 | 52322 186563 | 41122 22575 1128408 50.0 | 1.155 % | c | 106681 | 52322 186563 | 45234 26419 1344605 50.9 | 1.155 % | c | 112449 | 52322 186563 | 49758 32187 1751316 54.4 | 1.155 % | c | 121098 | 52322 186563 | 54734 40836 2149541 52.6 | 1.155 % | c ============================================================================== c [1mFound solution: 48598200[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 390314681 bits: 29/29 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 127352 | 52359 186889 | 17453 47090 2617772 55.6 | 1.155 % | c | 127452 | 52359 186889 | 19198 15669 758136 48.4 | 1.316 % | c | 127603 | 52359 186889 | 21118 15820 760395 48.1 | 1.316 % | c | 127830 | 52359 186889 | 23229 16047 769122 47.9 | 1.316 % | c | 128167 | 52359 186889 | 25552 16384 778109 47.5 | 1.316 % | c | 128674 | 52359 186889 | 28108 16891 790756 46.8 | 1.316 % | c | 129433 | 52359 186889 | 30919 17650 813409 46.1 | 1.316 % | c | 130572 | 52359 186889 | 34010 18789 865561 46.1 | 1.316 % | c | 132282 | 52359 186889 | 37412 20499 938830 45.8 | 1.316 % | c | 134845 | 52359 186889 | 41153 23062 1064072 46.1 | 1.316 % | c | 138691 | 52359 186889 | 45268 26908 1247411 46.4 | 1.316 % | c | 144457 | 52359 186889 | 49795 32674 1629064 49.9 | 1.316 % | c | 153106 | 52359 186889 | 54774 41323 1964251 47.5 | 1.316 % | c | 166082 | 52359 186889 | 60252 54299 4087971 75.3 | 1.316 % | c | 185543 | 52359 186889 | 66277 26698 1814676 68.0 | 1.316 % | c | 214736 | 52359 186889 | 72905 55891 5612823 100.4 | 1.316 % | c | 258526 | 52359 186889 | 80196 35150 5426643 154.4 | 1.316 % | c ============================================================================== c [1mFound solution: 44547717[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1378 maxlim: 346365164 bits: 29/29 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 321806 | 61657 220229 | 20552 29509 4096249 138.8 | 1.316 % | c | 321906 | 61642 220180 | 22607 13297 1753350 131.9 | 1.430 % | c | 322056 | 61642 220180 | 24867 13447 1754299 130.5 | 1.430 % | c | 322281 | 61642 220180 | 27354 13672 1755821 128.4 | 1.430 % | c | 322618 | 61642 220180 | 30090 14009 1758564 125.5 | 1.430 % | c | 323124 | 61642 220180 | 33099 14515 1765135 121.6 | 1.430 % | c | 323883 | 61642 220180 | 36409 15274 1786015 116.9 | 1.430 % | c | 325022 | 61642 220180 | 40050 16413 1802314 109.8 | 1.430 % | c | 326731 | 61642 220180 | 44055 18122 1840433 101.6 | 1.430 % | c | 329293 | 61550 219852 | 48460 20678 1908909 92.3 | 1.494 % | c | 333137 | 61550 219852 | 53306 24522 2028673 82.7 | 1.494 % | c | 338904 | 61550 219852 | 58637 30289 2315549 76.4 | 1.494 % | c | 347553 | 61541 219825 | 64500 38937 2744062 70.5 | 1.516 % | c | 360527 | 61505 219697 | 70951 51908 3464505 66.7 | 1.537 % | c ============================================================================== c [1mFound solution: 44546226[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2190 maxlim: 345462755 bits: 29/29 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 368761 | 76650 273861 | 25550 60142 4051496 67.4 | 1.537 % | c | 368862 | 76650 273861 | 28105 15623 1014216 64.9 | 1.417 % | c | 369012 | 76650 273861 | 30915 15773 1016609 64.5 | 1.417 % | c | 369239 | 76650 273861 | 34007 16000 1020990 63.8 | 1.417 % | c | 369576 | 76650 273861 | 37407 16337 1028496 63.0 | 1.417 % | c | 370082 | 76650 273861 | 41148 16843 1047728 62.2 | 1.417 % | c | 370843 | 76650 273861 | 45263 17604 1071639 60.9 | 1.417 % | c | 371984 | 76650 273861 | 49789 18745 1104286 58.9 | 1.417 % | c | 373692 | 76650 273861 | 54768 20453 1205464 58.9 | 1.417 % | c | 376255 | 76650 273861 | 60245 23016 1298019 56.4 | 1.417 % | c ============================================================================== c [1mFound solution: 15518352[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1246 maxlim: 130490629 bits: 28/27 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 379374 | 69349 248002 | 23116 21198 1073718 50.7 | 1.417 % | c | 379474 | 69349 248002 | 25427 21298 1074346 50.4 | 10.544 % | c | 379624 | 69349 248002 | 27970 21448 1092902 51.0 | 10.544 % | c | 379849 | 69349 248002 | 30767 21673 1094831 50.5 | 10.544 % | c | 380188 | 69349 248002 | 33844 22012 1101495 50.0 | 10.544 % | c | 380696 | 69343 247985 | 37228 22519 1109501 49.3 | 10.552 % | c | 381455 | 69304 247856 | 40951 23263 1123898 48.3 | 10.591 % | c | 382595 | 69304 247856 | 45046 24403 1162832 47.7 | 10.591 % | c | 384303 | 69296 247830 | 49551 26052 1181253 45.3 | 10.606 % | c ============================================================================== c [1mFound solution: 15514737[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2072 maxlim: 64733882 bits: 27/26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 386574 | 83675 299278 | 27891 28323 1246825 44.0 | 10.606 % | c | 386674 | 83675 299278 | 30680 28423 1247441 43.9 | 9.235 % | c | 386827 | 83675 299278 | 33748 28576 1249740 43.7 | 9.235 % | c | 387054 | 83675 299278 | 37122 28803 1254983 43.6 | 9.235 % | c | 387392 | 83675 299278 | 40835 29141 1264445 43.4 | 9.235 % | c | 387900 | 83675 299278 | 44918 29649 1274378 43.0 | 9.235 % | c | 388660 | 83675 299278 | 49410 30409 1297331 42.7 | 9.235 % | c | 389799 | 83675 299278 | 54351 31548 1340124 42.5 | 9.235 % | c | 391508 | 83675 299278 | 59786 33257 1414471 42.5 | 9.235 % | c | 394071 | 83675 299278 | 65765 35820 1491616 41.6 | 9.235 % | c | 397915 | 83675 299278 | 72342 39664 1978678 49.9 | 9.235 % | c | 403682 | 83675 299278 | 79576 45431 2241219 49.3 | 9.235 % | c ============================================================================== c [1mFound solution: 15510588[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 64738031 bits: 27/26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 407778 | 83689 299429 | 27896 49527 2491096 50.3 | 9.235 % | c | 407878 | 83689 299429 | 30685 15595 809103 51.9 | 9.271 % | c | 408028 | 83689 299429 | 33754 15745 810840 51.5 | 9.271 % | c | 408255 | 83689 299429 | 37129 15972 817040 51.2 | 9.271 % | c | 408592 | 83689 299429 | 40842 16309 827614 50.7 | 9.271 % | c | 409099 | 83689 299429 | 44926 16816 841455 50.0 | 9.271 % | c | 409860 | 83689 299429 | 49419 17577 861305 49.0 | 9.271 % | c | 411000 | 83689 299429 | 54361 18717 904651 48.3 | 9.271 % | c | 412708 | 83689 299429 | 59797 20425 939443 46.0 | 9.271 % | c | 415270 | 83689 299429 | 65777 22987 1173211 51.0 | 9.271 % | c | 419114 | 83689 299429 | 72355 26831 1277488 47.6 | 9.271 % | c ============================================================================== c [1mFound solution: 14953888[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 65294731 bits: 27/26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 421687 | 83704 299588 | 27901 29404 1414926 48.1 | 9.271 % | c | 421788 | 83704 299588 | 30691 14803 537064 36.3 | 9.319 % | c | 421938 | 83704 299588 | 33760 14953 538987 36.0 | 9.319 % | c | 422163 | 83704 299588 | 37136 15178 544374 35.9 | 9.319 % | c | 422501 | 83704 299588 | 40849 15516 551368 35.5 | 9.319 % | c | 423007 | 83704 299588 | 44934 16022 565299 35.3 | 9.319 % | c | 423766 | 83704 299588 | 49428 16781 590362 35.2 | 9.319 % | c | 424906 | 83704 299588 | 54371 17921 673819 37.6 | 9.319 % | c | 426615 | 83704 299588 | 59808 19630 719672 36.7 | 9.319 % | c | 429178 | 83696 299563 | 65789 22192 824706 37.2 | 9.332 % | c | 433023 | 83696 299563 | 72368 26037 969772 37.2 | 9.332 % | c | 438790 | 83690 299543 | 79604 31799 1432035 45.0 | 9.339 % | c | 447439 | 83690 299543 | 87565 40448 2079617 51.4 | 9.339 % | c | 460413 | 83690 299543 | 96321 53422 2806992 52.5 | 9.339 % | c | 479874 | 83637 299352 | 105954 72660 4728639 65.1 | 9.352 % | c | 509070 | 83637 299352 | 116549 101856 7699095 75.6 | 9.352 % | c | 552860 | 83630 299329 | 128204 38162 2810779 73.7 | 9.359 % | c ============================================================================== c [1mFound solution: 14953718[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 908 maxlim: 65294901 bits: 27/26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 557043 | 89912 321845 | 29970 42345 2992631 70.7 | 9.359 % | c | 557143 | 89912 321845 | 32967 13928 588100 42.2 | 8.897 % | c | 557294 | 89912 321845 | 36263 14079 590343 41.9 | 8.897 % | c | 557521 | 89912 321845 | 39890 14306 602706 42.1 | 8.897 % | c | 557862 | 89912 321845 | 43879 14647 607107 41.4 | 8.897 % | c | 558368 | 89912 321845 | 48266 15153 614334 40.5 | 8.897 % | c | 559127 | 89912 321845 | 53093 15912 630584 39.6 | 8.897 % | c | 560267 | 89912 321845 | 58403 17052 654924 38.4 | 8.897 % | c | 561975 | 89912 321845 | 64243 18760 730341 38.9 | 8.897 % | c | 564537 | 89912 321845 | 70667 21322 887333 41.6 | 8.897 % | c | 568381 | 89912 321845 | 77734 25166 1043652 41.5 | 8.897 % | c | 574147 | 89912 321845 | 85507 30932 1527411 49.4 | 8.897 % | c | 582796 | 89912 321845 | 94058 39581 1964291 49.6 | 8.897 % | c | 595770 | 89912 321845 | 103464 52555 3318199 63.1 | 8.897 % | c | 615231 | 89912 321845 | 113811 72016 5901878 82.0 | 8.897 % | c | 644424 | 89912 321845 | 125192 101209 8957059 88.5 | 8.897 % | c | 688214 | 89912 321845 | 137711 28474 2865984 100.7 | 8.897 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.85 0.97 0.91 2/54 3452 Raw data (stat): 3452 (runsolver) R 3451 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485667960 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 0.87 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 1805 0 0 0 993 5 0 0 25 0 1 0 485667960 9207808 1781 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2248 1781 603 41 0 2207 0 vsize: 8992 [startup+20.0001 s] Raw data (loadavg): 0.89 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 2700 0 0 0 1990 8 0 0 25 0 1 0 485667960 12955648 2676 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3163 2676 603 41 0 3122 0 vsize: 12652 [startup+30.0008 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 3379 0 0 0 2989 9 0 0 25 0 1 0 485667960 15769600 3355 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3850 3355 603 41 0 3809 0 vsize: 15400 [startup+40.0009 s] Raw data (loadavg): 0.92 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 3549 0 0 0 3989 10 0 0 25 0 1 0 485667960 16433152 3525 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4012 3525 603 41 0 3971 0 vsize: 16048 [startup+50.002 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 4375 0 0 0 4987 12 0 0 25 0 1 0 485667960 19791872 4351 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4832 4351 603 41 0 4791 0 vsize: 19328 [startup+60.0027 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 4970 0 0 0 5985 14 0 0 25 0 1 0 485667960 22200320 4946 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5420 4946 603 41 0 5379 0 vsize: 21680 [startup+70.0028 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 4970 0 0 0 6985 14 0 0 25 0 1 0 485667960 22200320 4946 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5420 4946 603 41 0 5379 0 vsize: 21680 [startup+80.0039 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5071 0 0 0 7985 15 0 0 25 0 1 0 485667960 22638592 5043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5043 603 41 0 5486 0 vsize: 22108 [startup+90.0045 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5071 0 0 0 8984 15 0 0 25 0 1 0 485667960 22638592 5043 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5043 603 41 0 5486 0 vsize: 22108 [startup+100.005 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5071 0 0 0 9984 15 0 0 25 0 1 0 485667960 22638592 5043 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5043 603 41 0 5486 0 vsize: 22108 [startup+110.006 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5075 0 0 0 10984 15 0 0 25 0 1 0 485667960 22638592 5047 4294967295 134512640 134672761 3221224544 3221223680 134556345 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5047 603 41 0 5486 0 vsize: 22108 [startup+120.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5075 0 0 0 11984 16 0 0 25 0 1 0 485667960 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5047 603 41 0 5486 0 vsize: 22108 [startup+130.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5075 0 0 0 12983 17 0 0 25 0 1 0 485667960 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5047 603 41 0 5486 0 vsize: 22108 [startup+140.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5075 0 0 0 13983 17 0 0 25 0 1 0 485667960 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5047 603 41 0 5486 0 vsize: 22108 [startup+150.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5075 0 0 0 14983 17 0 0 25 0 1 0 485667960 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5527 5047 603 41 0 5486 0 vsize: 22108 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 5860 0 0 0 15982 19 0 0 25 0 1 0 485667960 25731072 5832 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6282 5832 603 41 0 6241 0 vsize: 25128 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 6400 0 0 0 16980 20 0 0 25 0 1 0 485667960 27873280 6372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6805 6372 603 41 0 6764 0 vsize: 27220 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 6717 0 0 0 17979 22 0 0 25 0 1 0 485667960 29220864 6689 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7134 6689 603 41 0 7093 0 vsize: 28536 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 6717 0 0 0 18979 22 0 0 25 0 1 0 485667960 29220864 6689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7134 6689 603 41 0 7093 0 vsize: 28536 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 6717 0 0 0 19978 23 0 0 25 0 1 0 485667960 29220864 6689 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7134 6689 603 41 0 7093 0 vsize: 28536 [startup+210.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 6717 0 0 0 20978 23 0 0 25 0 1 0 485667960 29220864 6689 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7134 6689 603 41 0 7093 0 vsize: 28536 [startup+220.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 6717 0 0 0 21978 23 0 0 25 0 1 0 485667960 29220864 6689 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7134 6689 603 41 0 7093 0 vsize: 28536 [startup+230.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 7070 0 0 0 22977 24 0 0 25 0 1 0 485667960 30695424 7042 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7494 7042 603 41 0 7453 0 vsize: 29976 [startup+240.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 7826 0 0 0 23975 26 0 0 25 0 1 0 485667960 33775616 7798 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8246 7798 603 41 0 8205 0 vsize: 32984 [startup+250.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 8540 0 0 0 24973 29 0 0 25 0 1 0 485667960 36732928 8512 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8968 8512 603 41 0 8927 0 vsize: 35872 [startup+260.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 9427 0 0 0 25971 31 0 0 25 0 1 0 485667960 40493056 9399 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9886 9399 603 41 0 9845 0 vsize: 39544 [startup+270.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10254 0 0 0 26968 34 0 0 25 0 1 0 485667960 43864064 10226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10709 10226 603 41 0 10668 0 vsize: 42836 [startup+280.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 27966 36 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+290.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 28966 36 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+300.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 29966 36 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+310.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 30966 36 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+320.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 31966 37 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+330.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 32966 37 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+340.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 33966 37 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+350.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 34966 37 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+360.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 35966 38 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+370.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 10882 0 0 0 36966 38 0 0 25 0 1 0 485667960 46419968 10854 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10854 603 41 0 11292 0 vsize: 45332 [startup+380.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 11548 0 0 0 37964 40 0 0 25 0 1 0 485667960 49242112 11520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12022 11520 603 41 0 11981 0 vsize: 48088 [startup+390.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 12196 0 0 0 38962 41 0 0 25 0 1 0 485667960 51810304 12168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12649 12168 603 41 0 12608 0 vsize: 50596 [startup+400.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 12847 0 0 0 39960 44 0 0 25 0 1 0 485667960 54501376 12819 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13306 12819 603 41 0 13265 0 vsize: 53224 [startup+410.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13382 0 0 0 40959 45 0 0 25 0 1 0 485667960 56651776 13354 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13831 13354 603 41 0 13790 0 vsize: 55324 [startup+420.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13942 0 0 0 41957 47 0 0 25 0 1 0 485667960 58933248 13914 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14388 13914 603 41 0 14347 0 vsize: 57552 [startup+430.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13942 0 0 0 42957 48 0 0 25 0 1 0 485667960 58933248 13914 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14388 13914 603 41 0 14347 0 vsize: 57552 [startup+440.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13942 0 0 0 43957 48 0 0 25 0 1 0 485667960 58933248 13914 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14388 13914 603 41 0 14347 0 vsize: 57552 [startup+450.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13967 0 0 0 44957 48 0 0 25 0 1 0 485667960 59129856 13939 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14436 13939 603 41 0 14395 0 vsize: 57744 [startup+460.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13967 0 0 0 45956 48 0 0 25 0 1 0 485667960 59129856 13939 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14436 13939 603 41 0 14395 0 vsize: 57744 [startup+470.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13967 0 0 0 46956 49 0 0 25 0 1 0 485667960 59129856 13939 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14436 13939 603 41 0 14395 0 vsize: 57744 [startup+480.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 13967 0 0 0 47956 49 0 0 25 0 1 0 485667960 59129856 13939 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14436 13939 603 41 0 14395 0 vsize: 57744 [startup+490.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14007 0 0 0 48956 49 0 0 25 0 1 0 485667960 59392000 13979 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14500 13979 603 41 0 14459 0 vsize: 58000 [startup+500.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14032 0 0 0 49956 49 0 0 25 0 1 0 485667960 59392000 14004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14500 14004 603 41 0 14459 0 vsize: 58000 [startup+510.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14088 0 0 0 50956 50 0 0 25 0 1 0 485667960 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14058 603 41 0 14571 0 vsize: 58448 [startup+520.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14088 0 0 0 51955 50 0 0 25 0 1 0 485667960 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14058 603 41 0 14571 0 vsize: 58448 [startup+530.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14088 0 0 0 52955 50 0 0 25 0 1 0 485667960 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14058 603 41 0 14571 0 vsize: 58448 [startup+540.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14088 0 0 0 53955 50 0 0 25 0 1 0 485667960 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14058 603 41 0 14571 0 vsize: 58448 [startup+550.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14088 0 0 0 54955 51 0 0 25 0 1 0 485667960 59850752 14058 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14058 603 41 0 14571 0 vsize: 58448 [startup+560.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 55954 52 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223552 134565852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+570.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 56954 52 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+580.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 57954 52 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+590.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 58953 53 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+600.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 59953 53 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+610.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 60953 53 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223600 134565121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+620.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 61953 53 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+630.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 62953 54 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+640.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 63953 54 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+650.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 64953 54 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+660.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 65953 54 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+670.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 66952 55 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+680.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 67953 55 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+690.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14090 0 0 0 68953 55 0 0 25 0 1 0 485667960 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14060 603 41 0 14571 0 vsize: 58448 [startup+700.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14092 0 0 0 69952 55 0 0 25 0 1 0 485667960 59850752 14062 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14062 603 41 0 14571 0 vsize: 58448 [startup+710.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14095 0 0 0 70952 55 0 0 25 0 1 0 485667960 59850752 14065 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14065 603 41 0 14571 0 vsize: 58448 [startup+720.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14098 0 0 0 71952 55 0 0 25 0 1 0 485667960 59850752 14068 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14068 603 41 0 14571 0 vsize: 58448 [startup+730.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14100 0 0 0 72952 56 0 0 25 0 1 0 485667960 59850752 14070 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14070 603 41 0 14571 0 vsize: 58448 [startup+740.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14103 0 0 0 73952 56 0 0 25 0 1 0 485667960 59850752 14073 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14073 603 41 0 14571 0 vsize: 58448 [startup+750.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14106 0 0 0 74952 56 0 0 25 0 1 0 485667960 59850752 14076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14076 603 41 0 14571 0 vsize: 58448 [startup+760.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14109 0 0 0 75952 57 0 0 25 0 1 0 485667960 59850752 14079 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14079 603 41 0 14571 0 vsize: 58448 [startup+770.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14112 0 0 0 76952 57 0 0 25 0 1 0 485667960 59850752 14082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14082 603 41 0 14571 0 vsize: 58448 [startup+780.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14118 0 0 0 77951 57 0 0 25 0 1 0 485667960 59850752 14088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14088 603 41 0 14571 0 vsize: 58448 [startup+790.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14123 0 0 0 78951 57 0 0 25 0 1 0 485667960 59850752 14093 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14612 14093 603 41 0 14571 0 vsize: 58448 [startup+800.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14283 0 0 0 79950 58 0 0 25 0 1 0 485667960 60518400 14253 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14775 14253 603 41 0 14734 0 vsize: 59100 [startup+810.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14605 0 0 0 80948 61 0 0 25 0 1 0 485667960 61853696 14575 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14575 603 41 0 15060 0 vsize: 60404 [startup+820.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14605 0 0 0 81948 61 0 0 25 0 1 0 485667960 61853696 14575 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14575 603 41 0 15060 0 vsize: 60404 [startup+830.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14605 0 0 0 82948 61 0 0 25 0 1 0 485667960 61853696 14575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14575 603 41 0 15060 0 vsize: 60404 [startup+840.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14605 0 0 0 83948 61 0 0 25 0 1 0 485667960 61853696 14575 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14575 603 41 0 15060 0 vsize: 60404 [startup+850.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 84948 62 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+860.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 85948 62 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+870.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 86947 62 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+880.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 87947 63 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+890.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 88947 63 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+900.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 89947 63 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+910.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 90946 63 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+920.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 91946 64 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+930.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 92946 64 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+940.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 93946 64 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+950.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 94946 65 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+960.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 95946 65 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+970.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 96945 65 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+980.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 97945 65 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+990.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 98945 66 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 99945 66 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 100945 66 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 101945 67 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 102945 67 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 103944 67 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 104944 68 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 105944 68 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14620 0 0 0 106944 68 0 0 25 0 1 0 485667960 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15101 14590 603 41 0 15060 0 vsize: 60404 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 14822 0 0 0 107943 69 0 0 25 0 1 0 485667960 62660608 14792 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15298 14792 603 41 0 15257 0 vsize: 61192 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 15162 0 0 0 108943 70 0 0 25 0 1 0 485667960 64139264 15132 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15659 15132 603 41 0 15618 0 vsize: 62636 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 15441 0 0 0 109942 71 0 0 25 0 1 0 485667960 65208320 15411 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15920 15411 603 41 0 15879 0 vsize: 63680 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 15699 0 0 0 110941 72 0 0 25 0 1 0 485667960 66277376 15669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16181 15669 603 41 0 16140 0 vsize: 64724 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 15960 0 0 0 111940 72 0 0 25 0 1 0 485667960 67358720 15930 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16445 15930 603 41 0 16404 0 vsize: 65780 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16225 0 0 0 112939 73 0 0 25 0 1 0 485667960 68960256 16195 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16836 16195 603 41 0 16795 0 vsize: 67344 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 113939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 114939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 115939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 116939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 117939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 118939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3452 Raw data (stat): 3452 (minisat+) R 3451 22932 22931 0 -1 0 16428 0 0 0 119939 74 0 0 25 0 1 0 485667960 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17033 16398 603 41 0 16992 0 vsize: 68132 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 3452 Raw data (stat): 3452 (minisat+) Z 3451 22932 22931 0 -1 12 16431 0 0 0 119939 77 0 0 25 0 1 0 485667960 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.07 CPU time (s): 1200.17 CPU user time (s): 1199.4 CPU system time (s): 0.774882 CPU usage (%): 100.009 Max. virtual memory (Kb): 68132 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####