Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0282.opb |
MD5SUM | a733e9fa1e4e3ac90baf85249f7c3e9a |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01984 |
Number of variables | 282 |
Total number of constraints | 523 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 282 |
Number of constraints which are nor clauses,nor cardinality constraints | 64 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 57 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-05-25 18:54:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22118 boxname=wulflinc4 idbench=934 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0282.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0282.opb IDLAUNCH: 22118 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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.169 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: 924500 kB Buffers: 27668 kB Cached: 62476 kB SwapCached: 500 kB Active: 18868 kB Inactive: 73620 kB HighTotal: 131008 kB HighFree: 75684 kB LowTotal: 903652 kB LowFree: 848816 kB SwapTotal: 2097136 kB SwapFree: 2096004 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5784 kB Slab: 11948 kB Committed_AS: 71784 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 19:14:58 (client local time) WITH STATUS 152 IN 1229.86 SECONDS stats: 22118 7 1229.86 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 221 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss................................................................................................................................................................................. c ---[ 223]---> Sorter-cost: 850 Base: 5 2 3 3 c ---[ 222]---> Sorter-cost: 712 Base: 5 2 3 3 c ---[ 221]---> Sorter-cost: 1135 Base: 2 5 5 c ---[ 220]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 219]---> Sorter-cost: 1099 Base: 2 5 3 2 c ---[ 218]---> Sorter-cost: 882 Base: 2 5 3 3 c ---[ 217]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 216]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 215]---> Sorter-cost: 1016 Base: 2 5 3 c ---[ 214]---> Sorter-cost: 898 Base: 2 5 3 3 c ---[ 213]---> Sorter-cost: 1146 Base: 2 5 3 3 c ---[ 211]---> Sorter-cost: 996 Base: 2 5 3 3 c ---[ 209]---> Sorter-cost: 943 Base: 2 5 3 3 c ---[ 208]---> Sorter-cost: 760 Base: 2 5 3 3 c ---[ 207]---> Sorter-cost: 769 Base: 5 2 3 3 c ---[ 206]---> Sorter-cost: 713 Base: 5 2 3 3 c ---[ 205]---> Sorter-cost: 1005 Base: 2 5 5 c ---[ 204]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 203]---> Sorter-cost: 1072 Base: 2 5 3 c ---[ 202]---> Sorter-cost: 885 Base: 2 5 3 2 c ---[ 201]---> Sorter-cost: 712 Base: 5 2 3 3 c ---[ 199]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 198]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 197]---> Sorter-cost: 938 Base: 2 5 3 2 c ---[ 196]---> Sorter-cost: 852 Base: 2 5 3 3 c ---[ 195]---> Sorter-cost: 1059 Base: 2 5 3 3 c ---[ 194]---> Sorter-cost: 949 Base: 2 5 3 3 c ---[ 193]---> Sorter-cost: 844 Base: 2 5 3 3 c ---[ 192]---> Sorter-cost: 841 Base: 2 5 3 3 c ---[ 191]---> Sorter-cost: 1081 Base: 2 5 3 3 c ---[ 190]---> Sorter-cost: 996 Base: 2 5 3 2 c ---[ 189]---> Sorter-cost: 995 Base: 2 5 3 3 c ---[ 188]---> Sorter-cost: 985 Base: 2 5 3 2 c ---[ 187]---> BDD-cost: 56 c ---[ 186]---> BDD-cost: 10 c ---[ 185]---> BDD-cost: 56 c ---[ 184]---> BDD-cost: 56 c ---[ 183]---> BDD-cost: 16 c ---[ 182]---> BDD-cost: 26 c ---[ 181]---> BDD-cost: 8 c ---[ 180]---> BDD-cost: 4 c ---[ 2]---> Sorter-cost: 678 Base: 2 5 3 c ---[ 1]---> Sorter-cost: 694 Base: 2 5 3 c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 70255 164891 | 23418 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 881867[0m c ---[ 0]---> Sorter-cost:77310 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94 | 288858 675684 | 96286 88 654 7.4 | 0.000 % | c | 195 | 288627 675172 | 105914 184 1358 7.4 | 0.198 % | c | 347 | 288591 675094 | 116506 333 2602 7.8 | 0.208 % | c | 573 | 288578 675066 | 128156 558 4285 7.7 | 0.212 % | c ============================================================================== c [1mFound solution: 798158[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 595 | 289292 677295 | 96430 580 4464 7.7 | 0.212 % | c | 695 | 289229 677156 | 106073 677 5230 7.7 | 0.228 % | c | 845 | 289229 677156 | 116680 827 11071 13.4 | 0.228 % | c | 1070 | 289229 677156 | 128348 1052 12272 11.7 | 0.228 % | c | 1407 | 289229 677156 | 141183 1389 16783 12.1 | 0.228 % | c | 1913 | 289229 677156 | 155301 1895 22562 11.9 | 0.228 % | c | 2673 | 289075 676811 | 170831 2651 36393 13.7 | 0.268 % | c ============================================================================== c [1mFound solution: 491204[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3485 | 289830 678675 | 96610 3463 53869 15.6 | 0.268 % | c | 3588 | 289830 678675 | 106271 3566 56114 15.7 | 0.268 % | c | 3738 | 289830 678675 | 116898 3716 57041 15.4 | 0.268 % | c | 3964 | 289830 678675 | 128587 3942 58762 14.9 | 0.268 % | c | 4302 | 289497 677924 | 141446 4259 65556 15.4 | 0.359 % | c | 4808 | 289486 677901 | 155591 4764 76531 16.1 | 0.362 % | c | 5570 | 289486 677901 | 171150 5526 92145 16.7 | 0.362 % | c | 6709 | 289269 677414 | 188265 6660 147337 22.1 | 0.421 % | c | 8420 | 289226 677317 | 207092 8370 195883 23.4 | 0.433 % | c | 10982 | 288502 675683 | 227801 10882 251129 23.1 | 0.639 % | c | 14827 | 288119 674823 | 250581 14713 432249 29.4 | 0.746 % | c ============================================================================== c [1mFound solution: 436562[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16547 | 288672 676183 | 96224 16433 539492 32.8 | 0.746 % | c | 16647 | 288672 676183 | 105846 16533 540183 32.7 | 0.744 % | c | 16798 | 288672 676183 | 116431 16684 541629 32.5 | 0.744 % | c | 17024 | 288672 676183 | 128074 16910 550880 32.6 | 0.744 % | c | 17362 | 288672 676183 | 140881 17248 558318 32.4 | 0.744 % | c | 17868 | 288672 676183 | 154969 17754 566864 31.9 | 0.744 % | c | 18629 | 288542 675891 | 170466 18512 573030 31.0 | 0.778 % | c | 19768 | 288542 675891 | 187513 19651 616919 31.4 | 0.778 % | c | 21478 | 288517 675836 | 206264 21359 721335 33.8 | 0.785 % | c ============================================================================== c [1mFound solution: 435105[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22186 | 288522 676084 | 96174 22015 748548 34.0 | 0.785 % | c | 22286 | 288522 676084 | 105791 22115 750097 33.9 | 0.886 % | c | 22437 | 288522 676084 | 116370 22266 750817 33.7 | 0.886 % | c | 22662 | 288522 676084 | 128007 22491 752052 33.4 | 0.886 % | c | 22999 | 288522 676084 | 140808 22828 754156 33.0 | 0.886 % | c | 23505 | 288522 676084 | 154889 23334 777295 33.3 | 0.886 % | c | 24266 | 288458 675940 | 170378 24094 804215 33.4 | 0.902 % | c | 25405 | 288430 675876 | 187415 25231 822738 32.6 | 0.910 % | c | 27116 | 288321 675631 | 206157 26937 846652 31.4 | 0.940 % | c | 29681 | 288251 675472 | 226773 29492 1007488 34.2 | 0.960 % | c ============================================================================== c [1mFound solution: 376947[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31856 | 288251 675561 | 96083 31666 1138561 36.0 | 0.960 % | c | 31957 | 288251 675561 | 105691 31767 1139909 35.9 | 0.971 % | c | 32108 | 288251 675561 | 116260 31918 1140918 35.7 | 0.971 % | c | 32333 | 288145 675322 | 127886 32142 1144235 35.6 | 1.000 % | c | 32670 | 287939 674860 | 140675 32454 1155638 35.6 | 1.055 % | c | 33176 | 287939 674860 | 154742 32960 1220439 37.0 | 1.056 % | c | 33936 | 287939 674860 | 170216 33720 1267260 37.6 | 1.055 % | c | 35075 | 287807 674558 | 187238 34853 1287014 36.9 | 1.095 % | c ============================================================================== c [1mFound solution: 376622[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35698 | 287822 674602 | 95940 35476 1359098 38.3 | 1.095 % | c | 35798 | 287822 674602 | 105534 35576 1365673 38.4 | 1.096 % | c | 35949 | 287822 674602 | 116087 35727 1372000 38.4 | 1.096 % | c | 36174 | 287822 674602 | 127696 35952 1376958 38.3 | 1.096 % | c | 36512 | 287822 674602 | 140465 36290 1395290 38.4 | 1.096 % | c ============================================================================== c [1mFound solution: 354913[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36822 | 287792 674547 | 95930 36599 1404305 38.4 | 1.096 % | c | 36922 | 287792 674547 | 105523 36699 1405521 38.3 | 1.108 % | c | 37073 | 287792 674547 | 116075 36850 1406497 38.2 | 1.108 % | c | 37300 | 287792 674547 | 127682 37077 1420087 38.3 | 1.108 % | c | 37637 | 287792 674547 | 140451 37414 1438814 38.5 | 1.108 % | c | 38143 | 287792 674547 | 154496 37920 1448278 38.2 | 1.108 % | c | 38902 | 287682 674299 | 169945 38677 1480337 38.3 | 1.138 % | c | 40042 | 287644 674215 | 186940 39816 1638384 41.1 | 1.148 % | c | 41750 | 287644 674215 | 205634 41524 1686397 40.6 | 1.148 % | c | 44312 | 287644 674215 | 226197 44086 1953984 44.3 | 1.148 % | c | 48157 | 287510 673913 | 248817 47929 2297892 47.9 | 1.183 % | c ============================================================================== c [1mFound solution: 354908[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48837 | 287329 673517 | 95776 48605 2325753 47.9 | 1.183 % | c | 48937 | 287329 673517 | 105353 48705 2331070 47.9 | 1.232 % | c | 49087 | 287329 673517 | 115888 48855 2338335 47.9 | 1.232 % | c | 49312 | 287325 673508 | 127477 49079 2340723 47.7 | 1.233 % | c | 49649 | 287289 673426 | 140225 49415 2349449 47.5 | 1.244 % | c | 50156 | 287289 673426 | 154248 49922 2366434 47.4 | 1.244 % | c | 50915 | 287289 673426 | 169673 50681 2372878 46.8 | 1.244 % | c | 52055 | 287289 673426 | 186640 51821 2416696 46.6 | 1.244 % | c | 53763 | 287265 673372 | 205304 53528 2515819 47.0 | 1.252 % | c ============================================================================== c [1mFound solution: 354907[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54985 | 287199 673349 | 95733 54748 2617771 47.8 | 1.252 % | c | 55087 | 287199 673349 | 105306 54850 2618381 47.7 | 1.274 % | c | 55238 | 287102 673132 | 115836 54999 2628353 47.8 | 1.302 % | c | 55463 | 287102 673132 | 127420 55224 2648900 48.0 | 1.302 % | c | 55800 | 287102 673132 | 140162 55561 2658612 47.9 | 1.302 % | c | 56308 | 286962 672814 | 154178 56048 2666934 47.6 | 1.342 % | c | 57068 | 286958 672805 | 169596 56807 2740203 48.2 | 1.343 % | c | 58207 | 286941 672768 | 186556 57945 2841513 49.0 | 1.348 % | c | 59916 | 286941 672768 | 205212 59654 2921875 49.0 | 1.348 % | c | 62478 | 286920 672722 | 225733 62215 3171421 51.0 | 1.354 % | c ============================================================================== c [1mFound solution: 354893[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 64209 | 286932 672754 | 95644 63946 3295032 51.5 | 1.354 % | c | 64310 | 286932 672754 | 105208 64047 3295611 51.5 | 1.355 % | c | 64461 | 286932 672754 | 115729 64198 3303094 51.5 | 1.355 % | c | 64686 | 286932 672754 | 127302 64423 3312052 51.4 | 1.355 % | c | 65024 | 286932 672754 | 140032 64761 3314663 51.2 | 1.355 % | c | 65533 | 286932 672754 | 154035 65270 3354188 51.4 | 1.355 % | c | 66292 | 286932 672754 | 169439 66029 3386946 51.3 | 1.355 % | c | 67432 | 286932 672754 | 186383 67169 3429370 51.1 | 1.355 % | c | 69140 | 286932 672754 | 205021 68877 3498751 50.8 | 1.355 % | c ============================================================================== c [1mFound solution: 351999[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69370 | 286939 672772 | 95646 69107 3514837 50.9 | 1.355 % | c | 69470 | 286939 672772 | 105210 69207 3517481 50.8 | 1.356 % | c ============================================================================== c [1mFound solution: 325754[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69603 | 286918 672729 | 95639 69339 3525718 50.8 | 1.356 % | c | 69703 | 286892 672670 | 105202 69438 3526373 50.8 | 1.370 % | c | 69853 | 286892 672670 | 115723 69588 3547742 51.0 | 1.370 % | c | 70079 | 286892 672670 | 127295 69814 3569348 51.1 | 1.370 % | c | 70416 | 286892 672670 | 140025 70151 3584009 51.1 | 1.370 % | c | 70924 | 286892 672670 | 154027 70659 3654183 51.7 | 1.370 % | c | 71683 | 286892 672670 | 169430 71418 3667043 51.3 | 1.370 % | c | 72822 | 286847 672568 | 186373 72554 3696020 50.9 | 1.382 % | c | 74530 | 286730 672304 | 205010 74256 3740046 50.4 | 1.415 % | c | 77092 | 286632 672083 | 225511 76816 4009626 52.2 | 1.440 % | c ============================================================================== c [1mFound solution: 325267[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 79868 | 286603 672024 | 95534 79590 4117132 51.7 | 1.440 % | c | 79968 | 286505 671805 | 105087 79688 4120996 51.7 | 1.482 % | c | 80118 | 286505 671805 | 115596 79838 4127671 51.7 | 1.482 % | c | 80345 | 286505 671805 | 127155 80065 4142188 51.7 | 1.482 % | c ============================================================================== c [1mFound solution: 324891[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 80640 | 286523 671924 | 95507 80360 4169092 51.9 | 1.482 % | c | 80740 | 286523 671924 | 105057 80460 4169528 51.8 | 1.483 % | c | 80890 | 286523 671924 | 115563 80610 4174709 51.8 | 1.483 % | c | 81115 | 286523 671924 | 127119 80835 4178907 51.7 | 1.483 % | c | 81452 | 286523 671924 | 139831 81172 4190033 51.6 | 1.483 % | c | 81958 | 286523 671924 | 153814 81678 4215423 51.6 | 1.483 % | c | 82717 | 286523 671924 | 169196 82437 4248696 51.5 | 1.483 % | c | 83856 | 286523 671924 | 186116 83576 4378185 52.4 | 1.483 % | c | 85565 | 286472 671808 | 204727 85284 4571724 53.6 | 1.496 % | c | 88129 | 286472 671808 | 225200 87848 4870692 55.4 | 1.496 % | c | 91973 | 286472 671808 | 247720 91692 5330851 58.1 | 1.496 % | c ============================================================================== c [1mFound solution: 324675[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94793 | 286465 671793 | 95488 94511 5591844 59.2 | 1.496 % | c | 94894 | 286465 671793 | 105036 94612 5592545 59.1 | 1.504 % | c | 95044 | 286465 671793 | 115540 94762 5594717 59.0 | 1.504 % | c | 95269 | 286465 671793 | 127094 94987 5596716 58.9 | 1.504 % | c | 95606 | 286465 671793 | 139803 95324 5616092 58.9 | 1.504 % | c | 96113 | 286465 671793 | 153784 95831 5651619 59.0 | 1.504 % | c | 96872 | 286465 671793 | 169162 96590 5684967 58.9 | 1.504 % | c ============================================================================== c [1mFound solution: 322839[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97234 | 286471 671807 | 95490 96952 5711630 58.9 | 1.504 % | c | 97334 | 286471 671807 | 105039 97052 5717178 58.9 | 1.505 % | c | 97484 | 286471 671807 | 115542 97202 5734519 59.0 | 1.505 % | c | 97709 | 286471 671807 | 127097 97427 5742109 58.9 | 1.505 % | c | 98046 | 286471 671807 | 139806 97764 5793815 59.3 | 1.505 % | c | 98554 | 286471 671807 | 153787 98272 5827995 59.3 | 1.505 % | c | 99315 | 286471 671807 | 169166 99033 5883452 59.4 | 1.505 % | c | 100454 | 286471 671807 | 186082 100172 5970295 59.6 | 1.505 % | c | 102162 | 286471 671807 | 204691 101880 6133092 60.2 | 1.505 % | c ============================================================================== c [1mFound solution: 322838[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102452 | 286404 671657 | 95468 102169 6157887 60.3 | 1.505 % | c | 102552 | 286404 671657 | 105014 31986 1235638 38.6 | 1.526 % | c | 102705 | 286404 671657 | 115516 32139 1236710 38.5 | 1.526 % | c | 102930 | 286404 671657 | 127067 32364 1251376 38.7 | 1.526 % | c | 103267 | 286404 671657 | 139774 32701 1270087 38.8 | 1.526 % | c ============================================================================== c [1mFound solution: 322837[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 103418 | 286367 671574 | 95455 32851 1280341 39.0 | 1.526 % | c | 103519 | 286367 671574 | 105000 32952 1293027 39.2 | 1.540 % | c | 103669 | 286367 671574 | 115500 33102 1300251 39.3 | 1.540 % | c | 103895 | 286367 671574 | 127050 33328 1319175 39.6 | 1.540 % | c | 104232 | 286367 671574 | 139755 33665 1337270 39.7 | 1.540 % | c ============================================================================== c [1mFound solution: 322815[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104482 | 286377 671676 | 95459 33915 1366281 40.3 | 1.540 % | c | 104582 | 286377 671676 | 105004 34015 1372203 40.3 | 1.541 % | c | 104734 | 286377 671676 | 115505 34167 1378933 40.4 | 1.541 % | c | 104959 | 286377 671676 | 127055 34392 1386271 40.3 | 1.541 % | c | 105297 | 286377 671676 | 139761 34730 1407505 40.5 | 1.541 % | c | 105805 | 286377 671676 | 153737 35238 1445714 41.0 | 1.541 % | c ============================================================================== c [1mFound solution: 322803[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106109 | 286389 671708 | 95463 35542 1464879 41.2 | 1.541 % | c | 106209 | 286389 671708 | 105009 35642 1465756 41.1 | 1.542 % | c | 106359 | 286389 671708 | 115510 35792 1466498 41.0 | 1.542 % | c | 106585 | 286389 671708 | 127061 36018 1486837 41.3 | 1.542 % | c | 106923 | 286389 671708 | 139767 36356 1523724 41.9 | 1.542 % | c | 107429 | 286389 671708 | 153744 36862 1551729 42.1 | 1.542 % | c | 108189 | 286389 671708 | 169118 37622 1594362 42.4 | 1.542 % | c | 109329 | 286389 671708 | 186030 38762 1800693 46.5 | 1.542 % | c | 111038 | 286389 671708 | 204633 40471 1924175 47.5 | 1.542 % | c ============================================================================== c [1mFound solution: 322758[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 111639 | 286398 671731 | 95466 41072 1983502 48.3 | 1.542 % | c | 111741 | 286398 671731 | 105012 41174 1991568 48.4 | 1.543 % | c | 111892 | 286398 671731 | 115513 41325 1999481 48.4 | 1.543 % | c | 112120 | 286398 671731 | 127065 41553 2036891 49.0 | 1.543 % | c | 112460 | 286392 671717 | 139771 41892 2039196 48.7 | 1.545 % | c | 112967 | 286249 671395 | 153748 42358 2072777 48.9 | 1.583 % | c ============================================================================== c [1mFound solution: 322756[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 113407 | 286258 671420 | 95419 42798 2163613 50.6 | 1.583 % | c | 113507 | 286258 671420 | 104960 42898 2164127 50.4 | 1.583 % | c | 113658 | 286258 671420 | 115456 43049 2168960 50.4 | 1.583 % | c | 113884 | 286258 671420 | 127002 43275 2185067 50.5 | 1.583 % | c ============================================================================== c [1mFound solution: 322749[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 114012 | 286267 671443 | 95422 43403 2215288 51.0 | 1.583 % | c | 114113 | 286267 671443 | 104964 43504 2217181 51.0 | 1.584 % | c | 114264 | 286237 671377 | 115460 43654 2230119 51.1 | 1.592 % | c | 114490 | 286237 671377 | 127006 43880 2242532 51.1 | 1.592 % | c | 114829 | 286237 671377 | 139707 44219 2259868 51.1 | 1.592 % | c | 115337 | 286233 671369 | 153678 44726 2305115 51.5 | 1.594 % | c ============================================================================== c [1mFound solution: 321363[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115687 | 286244 671397 | 95414 45076 2358047 52.3 | 1.594 % | c | 115787 | 286244 671397 | 104955 45176 2358575 52.2 | 1.595 % | c | 115938 | 286244 671397 | 115450 45327 2365104 52.2 | 1.595 % | c ============================================================================== c [1mFound solution: 321360[0m c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 116085 | 286258 671432 | 95419 45474 2385540 52.5 | 1.595 % | c | 116185 | 286258 671432 | 104960 45574 2387910 52.4 | 1.596 % | c | 116337 | 286258 671432 | 115456 45726 2399983 52.5 | 1.596 % | c | 116563 | 286258 671432 | 127002 45952 2434724 53.0 | 1.596 % | c | 116900 | 286237 671386 | 139702 46288 2472885 53.4 | 1.602 % | c | 117406 | 286237 671386 | 153673 46794 2485584 53.1 | 1.602 % | c ============================================================================== c [1mFound solution: 319923[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118136 | 286211 671329 | 95403 47523 2581249 54.3 | 1.602 % | c | 118237 | 286211 671329 | 104943 47624 2582560 54.2 | 1.612 % | c | 118389 | 286211 671329 | 115437 47776 2590145 54.2 | 1.612 % | c | 118614 | 286211 671329 | 126981 48001 2612706 54.4 | 1.612 % | c | 118956 | 286211 671329 | 139679 48343 2625316 54.3 | 1.612 % | c | 119463 | 286211 671329 | 153647 48850 2652967 54.3 | 1.612 % | c | 120223 | 286211 671329 | 169012 49610 2714939 54.7 | 1.612 % | c | 121362 | 286211 671329 | 185913 50749 2870613 56.6 | 1.612 % | c ============================================================================== c [1mFound solution: 318464[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 122535 | 286224 671362 | 95408 51922 2972933 57.3 | 1.612 % | c | 122636 | 286224 671362 | 104948 52023 2978542 57.3 | 1.613 % | c | 122786 | 286224 671362 | 115443 52173 2987829 57.3 | 1.613 % | c | 123011 | 286224 671362 | 126988 52398 3006530 57.4 | 1.613 % | c | 123348 | 286224 671362 | 139686 52735 3030391 57.5 | 1.613 % | c | 123854 | 286224 671362 | 153655 53241 3057847 57.4 | 1.613 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 4458 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.91 0.95 0.93 2/54 4454 Raw data (stat): 4454 (runsolver) R 4453 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782967321 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10 s] Raw data (loadavg): 0.92 0.95 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0001 s] Raw data (loadavg): 0.93 0.95 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0008 s] Raw data (loadavg): 0.94 0.95 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0006 s] Raw data (loadavg): 0.95 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0008 s] Raw data (loadavg): 0.96 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0013 s] Raw data (loadavg): 0.96 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0012 s] Raw data (loadavg): 0.97 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0023 s] Raw data (loadavg): 0.97 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0019 s] Raw data (loadavg): 0.98 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.98 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.98 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.98 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.99 0.96 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.93 2/55 4458 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.07 0.99 0.94 2/58 4510 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.06 0.99 0.94 2/55 4511 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.05 0.99 0.94 2/55 4511 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.04 0.99 0.94 2/55 4511 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.04 0.99 0.94 2/55 4511 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.03 0.99 0.94 2/55 4511 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.03 0.99 0.94 2/55 4511 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.01 0.99 0.94 3/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.015 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4513 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.74 s] Raw data (loadavg): 1.00 0.99 0.94 1/53 4515 Raw data (stat): 4454 (minisat+_script) S 4453 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782967321 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.74 CPU time (s): 1229.86 CPU user time (s): 1229.31 CPU system time (s): 0.555915 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####