Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8b3.opb |
MD5SUM | b2547f396d5cd0589545f2e597f6c86a |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 507 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1632 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1632 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1632 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.06684 |
Number of variables | 1632 |
Total number of constraints | 6924 |
Number of constraints which are clauses | 6924 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 8 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-14 04:01:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4681 boxname=wulflinc22 idbench=169 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b2547f396d5cd0589545f2e597f6c86a /oldhome/oroussel/tmp/wulflinc22/normalized-ii8b3.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-ii8b3.opb /oldhome/oroussel/tmp/wulflinc22/normalized-ii8b3.opb IDLAUNCH: 4681 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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: 827532 kB Buffers: 33276 kB Cached: 130692 kB SwapCached: 524 kB Active: 50928 kB Inactive: 116392 kB HighTotal: 131008 kB HighFree: 6580 kB LowTotal: 903652 kB LowFree: 820952 kB SwapTotal: 2097892 kB SwapFree: 2097368 kB Dirty: 52 kB Writeback: 0 kB Mapped: 6924 kB Slab: 34236 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 04:21:53 (client local time) WITH STATUS 10 IN 1200.32 SECONDS stats: 4681 7 1200.32 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 6924 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 6924 15408 | 2308 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 586[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:91716 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3 | 234997 548640 | 78332 3 28 9.3 | 0.000 % | c | 103 | 234380 547242 | 86165 94 1617 17.2 | 0.241 % | c | 253 | 232981 544055 | 94781 209 2402 11.5 | 0.813 % | c | 478 | 226813 529905 | 104259 312 18118 58.1 | 3.228 % | c | 815 | 221116 516824 | 114685 582 30280 52.0 | 5.472 % | c | 1322 | 217801 509243 | 126154 1045 52274 50.0 | 6.697 % | c | 2081 | 202026 472979 | 138769 1562 62449 40.0 | 13.021 % | c | 3220 | 192172 450257 | 152646 2477 111994 45.2 | 16.961 % | c | 4928 | 178087 417753 | 167911 3972 158969 40.0 | 22.707 % | c | 7491 | 156444 367717 | 184702 6168 270247 43.8 | 31.645 % | c | 11337 | 139427 328379 | 203173 9471 378882 40.0 | 38.671 % | c | 17103 | 118842 280735 | 223490 14739 666159 45.2 | 47.221 % | c | 25752 | 102008 241753 | 245839 22874 936735 41.0 | 54.212 % | c | 38726 | 99626 236254 | 270423 35752 1824735 51.0 | 55.171 % | c ============================================================================== c [1mFound solution: 585[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43613 | 99355 235656 | 33118 40626 2000362 49.2 | 55.171 % | c | 43714 | 99258 235433 | 36429 40726 2001914 49.2 | 55.337 % | c | 43864 | 99131 235140 | 40072 40852 2003818 49.1 | 55.389 % | c | 44089 | 99028 234899 | 44080 41069 2010452 49.0 | 55.435 % | c | 44426 | 98923 234653 | 48488 41391 2016167 48.7 | 55.483 % | c | 44932 | 98923 234653 | 53336 41897 2027056 48.4 | 55.483 % | c | 45692 | 98923 234653 | 58670 42657 2056398 48.2 | 55.483 % | c | 46831 | 98915 234635 | 64537 43794 2103421 48.0 | 55.486 % | c | 48539 | 98622 233951 | 70991 45263 2167464 47.9 | 55.617 % | c | 51101 | 98194 232955 | 78090 47734 2241462 47.0 | 55.803 % | c ============================================================================== c [1mFound solution: 584[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54168 | 98145 232836 | 32715 49447 2162053 43.7 | 55.803 % | c | 54269 | 98145 232836 | 35986 49548 2163544 43.7 | 55.817 % | c | 54419 | 98145 232836 | 39585 49698 2165649 43.6 | 55.817 % | c | 54646 | 98145 232836 | 43543 49925 2172336 43.5 | 55.817 % | c | 54983 | 98145 232836 | 47898 50262 2181794 43.4 | 55.817 % | c | 55489 | 98145 232836 | 52687 50768 2192521 43.2 | 55.817 % | c | 56248 | 97834 232119 | 57956 51125 2204499 43.1 | 55.944 % | c ============================================================================== c [1mFound solution: 583[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 56776 | 97908 232313 | 32636 51653 2212668 42.8 | 55.944 % | c | 56877 | 97908 232313 | 35899 51754 2213790 42.8 | 55.932 % | c | 57027 | 97908 232313 | 39489 51904 2216603 42.7 | 55.932 % | c | 57253 | 97827 232125 | 43438 52120 2218069 42.6 | 55.967 % | c | 57590 | 97827 232125 | 47782 52457 2225365 42.4 | 55.967 % | c | 58096 | 97827 232125 | 52560 52963 2230359 42.1 | 55.967 % | c | 58855 | 97827 232125 | 57816 53722 2249195 41.9 | 55.967 % | c | 59994 | 97827 232125 | 63598 54861 2293068 41.8 | 55.967 % | c ============================================================================== c [1mFound solution: 582[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 60747 | 97773 231991 | 32591 55593 2318943 41.7 | 55.967 % | c | 60847 | 97773 231991 | 35850 55693 2320357 41.7 | 55.982 % | c | 60997 | 97773 231991 | 39435 55843 2322740 41.6 | 55.982 % | c | 61222 | 97537 231444 | 43378 56034 2336448 41.7 | 56.082 % | c | 61560 | 97537 231444 | 47716 56372 2359219 41.9 | 56.082 % | c | 62066 | 97491 231338 | 52488 56871 2373677 41.7 | 56.100 % | c | 62827 | 97265 230811 | 57736 57626 2396121 41.6 | 56.200 % | c | 63966 | 97265 230811 | 63510 58765 2528609 43.0 | 56.200 % | c | 65675 | 97265 230811 | 69861 60474 2618102 43.3 | 56.200 % | c ============================================================================== c [1mFound solution: 581[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 67958 | 97348 231026 | 32449 62757 2709349 43.2 | 56.200 % | c | 68058 | 97348 231026 | 35693 62857 2710686 43.1 | 56.185 % | c | 68208 | 97348 231026 | 39263 63007 2720927 43.2 | 56.185 % | c | 68433 | 97348 231026 | 43189 63232 2724086 43.1 | 56.185 % | c | 68770 | 97348 231026 | 47508 63569 2739965 43.1 | 56.185 % | c | 69276 | 97348 231026 | 52259 64075 2756222 43.0 | 56.185 % | c | 70035 | 97348 231026 | 57485 64834 2857728 44.1 | 56.185 % | c | 71174 | 97348 231026 | 63233 65973 2926840 44.4 | 56.185 % | c | 72882 | 97348 231026 | 69557 67681 3000036 44.3 | 56.185 % | c | 75444 | 96438 228918 | 76513 70035 3141300 44.9 | 56.568 % | c | 79290 | 96228 228432 | 84164 73865 3345166 45.3 | 56.657 % | c ============================================================================== c [1mFound solution: 580[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 82209 | 95877 227605 | 31959 76146 3417706 44.9 | 56.657 % | c | 82310 | 95877 227605 | 35154 25138 724402 28.8 | 56.801 % | c | 82460 | 95877 227605 | 38670 25288 726598 28.7 | 56.801 % | c | 82685 | 95877 227605 | 42537 25513 730553 28.6 | 56.801 % | c | 83022 | 95877 227605 | 46791 25850 735460 28.5 | 56.801 % | c | 83529 | 95837 227512 | 51470 26356 750011 28.5 | 56.818 % | c | 84288 | 95837 227512 | 56617 27115 769226 28.4 | 56.818 % | c | 85427 | 95837 227512 | 62279 28254 853765 30.2 | 56.818 % | c | 87135 | 95430 226571 | 68506 29899 907510 30.4 | 56.987 % | c | 89697 | 95327 226332 | 75357 32458 1001968 30.9 | 57.031 % | c | 93541 | 95218 226078 | 82893 36285 1152408 31.8 | 57.078 % | c ============================================================================== c [1mFound solution: 579[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97622 | 94880 225317 | 31626 40335 1292669 32.0 | 57.078 % | c | 97722 | 94880 225317 | 34788 40435 1313991 32.5 | 57.241 % | c | 97872 | 94880 225317 | 38267 40585 1318326 32.5 | 57.241 % | c | 98098 | 94880 225317 | 42094 40811 1326047 32.5 | 57.241 % | c | 98435 | 94880 225317 | 46303 41148 1329867 32.3 | 57.241 % | c | 98941 | 94880 225317 | 50933 41654 1343719 32.3 | 57.241 % | c | 99700 | 94679 224853 | 56027 42387 1369844 32.3 | 57.322 % | c | 100840 | 94679 224853 | 61630 43527 1545654 35.5 | 57.322 % | c | 102548 | 94679 224853 | 67793 45235 1651697 36.5 | 57.322 % | c | 105111 | 94679 224853 | 74572 47798 1819388 38.1 | 57.322 % | c ============================================================================== c [1mFound solution: 578[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106061 | 94622 224707 | 31540 48706 1883634 38.7 | 57.322 % | c | 106161 | 94618 224698 | 34694 48805 1884189 38.6 | 57.340 % | c | 106311 | 94618 224698 | 38163 48955 1887875 38.6 | 57.340 % | c | 106537 | 94618 224698 | 41979 49181 1895146 38.5 | 57.340 % | c | 106875 | 94618 224698 | 46177 49519 1903486 38.4 | 57.340 % | c | 107382 | 94618 224698 | 50795 50026 1911698 38.2 | 57.340 % | c | 108142 | 94618 224698 | 55875 50786 1946211 38.3 | 57.340 % | c | 109281 | 94618 224698 | 61462 51925 2066014 39.8 | 57.340 % | c | 110990 | 94618 224698 | 67608 53634 2138315 39.9 | 57.340 % | c ============================================================================== c [1mFound solution: 577[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 112003 | 94701 224913 | 31567 54647 2199162 40.2 | 57.340 % | c | 112103 | 94592 224661 | 34723 54737 2199832 40.2 | 57.370 % | c | 112253 | 94323 224035 | 38196 54766 2200721 40.2 | 57.488 % | c | 112478 | 94323 224035 | 42015 54991 2202732 40.1 | 57.488 % | c | 112815 | 94109 223536 | 46217 55321 2208490 39.9 | 57.583 % | c | 113321 | 94109 223536 | 50838 55827 2216910 39.7 | 57.583 % | c | 114080 | 94109 223536 | 55922 56586 2234853 39.5 | 57.583 % | c | 115219 | 94109 223536 | 61515 57725 2292483 39.7 | 57.583 % | c | 116927 | 94109 223536 | 67666 59433 2389507 40.2 | 57.583 % | c | 119490 | 94109 223536 | 74433 61996 2591124 41.8 | 57.583 % | c | 123334 | 94109 223536 | 81876 65840 3534596 53.7 | 57.583 % | c | 129100 | 94109 223536 | 90064 71606 4014272 56.1 | 57.583 % | c | 137750 | 93828 222882 | 99070 80105 5498484 68.6 | 57.705 % | c ============================================================================== c [1mFound solution: 576[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 150672 | 93354 221761 | 31118 90773 6189313 68.2 | 57.705 % | c | 150773 | 93354 221761 | 34229 26519 1134042 42.8 | 57.903 % | c | 150924 | 93354 221761 | 37652 26670 1137380 42.6 | 57.903 % | c | 151149 | 93193 221383 | 41418 26864 1139970 42.4 | 57.976 % | c | 151490 | 93193 221383 | 45559 27205 1145643 42.1 | 57.976 % | c | 151997 | 93189 221374 | 50115 27707 1175191 42.4 | 57.977 % | c | 152757 | 93189 221374 | 55127 28467 1193931 41.9 | 57.977 % | c | 153898 | 93189 221374 | 60640 29608 1395056 47.1 | 57.977 % | c | 155606 | 93106 221183 | 66704 31315 1583730 50.6 | 58.011 % | c | 158168 | 93106 221183 | 73374 33877 1833405 54.1 | 58.011 % | c | 162012 | 93106 221183 | 80712 37721 2037970 54.0 | 58.011 % | c ============================================================================== c [1mFound solution: 575[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 165574 | 93176 221366 | 31058 41283 2237992 54.2 | 58.011 % | c | 165674 | 92950 220840 | 34163 41367 2239201 54.1 | 58.097 % | c | 165824 | 92950 220840 | 37580 41517 2243942 54.0 | 58.097 % | c | 166050 | 92950 220840 | 41338 41743 2246013 53.8 | 58.097 % | c | 166387 | 92950 220840 | 45472 42080 2255705 53.6 | 58.097 % | c | 166894 | 92950 220840 | 50019 42587 2264199 53.2 | 58.097 % | c | 167653 | 92942 220821 | 55021 43344 2329007 53.7 | 58.101 % | c | 168792 | 92942 220821 | 60523 44483 2360982 53.1 | 58.101 % | c | 170500 | 92017 218666 | 66575 46150 2427691 52.6 | 58.501 % | c ============================================================================== c [1mFound solution: 574[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 172957 | 91965 218530 | 30655 48593 2514260 51.7 | 58.501 % | c | 173058 | 91953 218502 | 33720 48691 2515253 51.7 | 58.523 % | c | 173208 | 91953 218502 | 37092 48841 2519042 51.6 | 58.523 % | c | 173434 | 91953 218502 | 40801 49067 2538513 51.7 | 58.523 % | c | 173772 | 91850 218260 | 44881 49393 2553486 51.7 | 58.571 % | c | 174278 | 91850 218260 | 49370 49899 2569012 51.5 | 58.571 % | c | 175037 | 91642 217773 | 54307 50648 2623632 51.8 | 58.665 % | c | 176177 | 91642 217773 | 59737 51788 2686002 51.9 | 58.665 % | c ============================================================================== c [1mFound solution: 573[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 177596 | 91715 217961 | 30571 53207 2758507 51.8 | 58.665 % | c | 177696 | 91715 217961 | 33628 53307 2761199 51.8 | 58.652 % | c | 177846 | 91715 217961 | 36990 53457 2763862 51.7 | 58.652 % | c | 178072 | 91715 217961 | 40690 53683 2768194 51.6 | 58.652 % | c | 178410 | 91715 217961 | 44759 54021 2787231 51.6 | 58.652 % | c | 178917 | 91715 217961 | 49234 54528 2804404 51.4 | 58.652 % | c | 179676 | 91711 217952 | 54158 55286 2833427 51.3 | 58.654 % | c | 180815 | 91711 217952 | 59574 56425 2908019 51.5 | 58.654 % | c | 182523 | 91665 217845 | 65531 58116 3031403 52.2 | 58.673 % | c ============================================================================== c [1mFound solution: 572[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 182826 | 91559 217580 | 30519 58279 3016486 51.8 | 58.673 % | c | 182926 | 91559 217580 | 33570 58379 3019991 51.7 | 58.714 % | c | 183076 | 91559 217580 | 36927 58529 3022603 51.6 | 58.714 % | c | 183301 | 91559 217580 | 40620 58754 3031064 51.6 | 58.714 % | c | 183640 | 91559 217580 | 44682 59093 3057475 51.7 | 58.714 % | c | 184146 | 91539 217534 | 49151 59595 3068321 51.5 | 58.722 % | c | 184908 | 91347 217089 | 54066 60323 3082119 51.1 | 58.803 % | c | 186048 | 91347 217089 | 59472 61463 3206690 52.2 | 58.803 % | c | 187756 | 91347 217089 | 65420 63171 3280577 51.9 | 58.803 % | c | 190318 | 91347 217089 | 71962 65733 3554174 54.1 | 58.803 % | c ============================================================================== c [1mFound solution: 571[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 191949 | 91414 217263 | 30471 67364 3690149 54.8 | 58.803 % | c | 192049 | 91374 217169 | 33518 67448 3699059 54.8 | 58.810 % | c | 192199 | 91374 217169 | 36869 67598 3700926 54.7 | 58.810 % | c | 192425 | 91374 217169 | 40556 67824 3728824 55.0 | 58.810 % | c | 192763 | 91374 217169 | 44612 68162 3742419 54.9 | 58.810 % | c | 193269 | 91374 217169 | 49073 68668 3773887 55.0 | 58.810 % | c | 194028 | 91374 217169 | 53981 69427 3815163 55.0 | 58.810 % | c | 195170 | 91374 217169 | 59379 70569 3866470 54.8 | 58.810 % | c ============================================================================== c [1mFound solution: 570[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 196356 | 90967 216199 | 30322 71627 3923971 54.8 | 58.810 % | c | 196456 | 90967 216199 | 33354 71727 3938020 54.9 | 58.983 % | c | 196608 | 90967 216199 | 36689 71879 3941004 54.8 | 58.983 % | c | 196833 | 90949 216157 | 40358 72096 3946536 54.7 | 58.990 % | c | 197170 | 90949 216157 | 44394 72433 3951319 54.6 | 58.990 % | c | 197676 | 90949 216157 | 48833 72939 3989532 54.7 | 58.990 % | c | 198435 | 90949 216157 | 53717 73698 4034470 54.7 | 58.990 % | c | 199574 | 90858 215944 | 59088 74835 4088934 54.6 | 59.032 % | c | 201282 | 90858 215944 | 64997 76543 4183411 54.7 | 59.032 % | c ============================================================================== c [1mFound solution: 569[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 202424 | 90930 216129 | 30310 77685 4230747 54.5 | 59.032 % | c | 202524 | 90930 216129 | 33341 32288 867116 26.9 | 59.019 % | c | 202675 | 90930 216129 | 36675 32439 868476 26.8 | 59.019 % | c | 202900 | 90766 215750 | 40342 32656 871770 26.7 | 59.087 % | c | 203237 | 90766 215750 | 44376 32993 879509 26.7 | 59.087 % | c | 203743 | 90766 215750 | 48814 33499 931462 27.8 | 59.087 % | c | 204502 | 90766 215750 | 53696 34258 953071 27.8 | 59.087 % | c | 205642 | 90766 215750 | 59065 35398 1001287 28.3 | 59.087 % | c | 207350 | 90562 215275 | 64972 37094 1065293 28.7 | 59.177 % | c | 209912 | 90546 215238 | 71469 39650 1120951 28.3 | 59.183 % | c ============================================================================== c [1mFound solution: 563[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 212241 | 90492 215145 | 30164 41962 1222088 29.1 | 59.183 % | c | 212341 | 90492 215145 | 33180 42062 1223210 29.1 | 59.242 % | c | 212492 | 90492 215145 | 36498 42213 1224690 29.0 | 59.242 % | c | 212718 | 90492 215145 | 40148 42439 1235119 29.1 | 59.242 % | c | 213055 | 90492 215145 | 44163 42776 1240756 29.0 | 59.242 % | c | 213561 | 90492 215145 | 48579 43282 1251985 28.9 | 59.242 % | c | 214320 | 89838 213632 | 53437 43962 1288826 29.3 | 59.514 % | c | 215460 | 89838 213632 | 58781 45102 1404856 31.1 | 59.514 % | c ============================================================================== c [1mFound solution: 562[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 216040 | 89787 213501 | 29929 45567 1433305 31.5 | 59.514 % | c | 216141 | 89787 213501 | 32921 45668 1434615 31.4 | 59.531 % | c | 216291 | 89787 213501 | 36214 45818 1436949 31.4 | 59.531 % | c | 216516 | 89787 213501 | 39835 46043 1444097 31.4 | 59.531 % | c | 216855 | 89787 213501 | 43819 46382 1462116 31.5 | 59.531 % | c | 217362 | 89787 213501 | 48200 46889 1477087 31.5 | 59.531 % | c | 218121 | 89755 213427 | 53021 47604 1497735 31.5 | 59.544 % | c | 219261 | 89116 211944 | 58323 46084 1493320 32.4 | 59.818 % | c | 220969 | 89112 211935 | 64155 47790 1603041 33.5 | 59.819 % | c ============================================================================== c [1mFound solution: 561[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 223504 | 89067 211847 | 29689 50315 1738734 34.6 | 59.819 % | c | 223604 | 89067 211847 | 32657 50415 1743280 34.6 | 59.857 % | c | 223754 | 89067 211847 | 35923 50565 1745336 34.5 | 59.857 % | c | 223980 | 88975 211628 | 39516 50784 1753890 34.5 | 59.901 % | c | 224319 | 88965 211605 | 43467 51115 1757410 34.4 | 59.905 % | c | 224825 | 88965 211605 | 47814 51621 1801074 34.9 | 59.905 % | c | 225585 | 88965 211605 | 52595 52381 1890677 36.1 | 59.905 % | c | 226724 | 88965 211605 | 57855 53520 1992368 37.2 | 59.905 % | c | 228434 | 88866 211374 | 63641 55227 2054282 37.2 | 59.949 % | c | 230996 | 88866 211374 | 70005 57789 2240224 38.8 | 59.949 % | c | 234840 | 88788 211193 | 77005 61432 2646269 43.1 | 59.981 % | c | 240607 | 88662 210903 | 84706 67101 3198529 47.7 | 60.033 % | c ============================================================================== c [1mFound solution: 553[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 245647 | 88876 211434 | 29625 72141 3892338 54.0 | 60.033 % | c | 245747 | 88876 211434 | 32587 72241 3897673 54.0 | 59.991 % | c | 245898 | 88876 211434 | 35846 72392 3917744 54.1 | 59.991 % | c | 246125 | 88492 210541 | 39430 72557 3924409 54.1 | 60.157 % | c | 246462 | 88492 210541 | 43373 72894 3940911 54.1 | 60.157 % | c | 246969 | 88492 210541 | 47711 73401 3951779 53.8 | 60.157 % | c | 247728 | 88468 210486 | 52482 74099 3980709 53.7 | 60.166 % | c | 248867 | 88468 210486 | 57730 75238 4047721 53.8 | 60.166 % | c c *** TERMINATED *** s SATISFIABLE v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 -x37 x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 -x73 x74 x75 -x76 x77 -x78 -x79 x80 x81 -x82 -x83 x84 -x85 x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 -x95 -x96 x97 -x98 x99 -x100 -x101 x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 -x157 x158 x159 -x160 x161 -x162 x163 -x164 -x165 x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 -x193 x194 -x195 x196 -x197 x198 -x199 x200 x201 -x202 -x203 x204 -x205 -x206 x207 -x208 -x209 x210 -x211 -x212 -x213 x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 x222 -x223 -x224 x225 -x226 -x227 x228 x229 -x230 -x231 -x232 -x233 x234 -x235 -x236 -x237 x238 -x239 -x240 -x241 -x242 x243 -x244 -x245 x246 -x247 -x248 -x249 x250 -x251 -x252 -x253 -x254 x255 -x256 -x257 x258 -x259 -x260 -x261 -x262 -x263 -x264 x265 -x266 -x267 x268 -x269 x270 -x271 -x272 -x273 x274 -x275 -x276 -x277 -x278 x279 -x280 -x281 x282 -x283 x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 x294 -x295 -x296 -x297 x298 x299 -x300 -x301 -x302 x303 -x304 -x305 x306 -x307 -x308 -x309 -x310 -x311 -x312 x313 -x314 x315 -x316 -x317 x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 x326 -x327 x328 -x329 x330 -x331 x332 x333 -x334 -x335 x336 -x337 -x338 x339 -x340 -x341 x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 x354 x355 -x356 -x357 -x358 -x359 -x360 x361 -x362 -x363 -x364 -x365 x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 x374 -x375 x376 -x377 x378 -x379 x380 x381 -x382 -x383 x384 -x385 x386 x387 -x388 -x389 x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 x402 x403 -x404 -x405 x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 x414 x415 -x416 -x417 -x418 -x419 -x420 x421 -x422 -x423 -x424 -x425 x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 x434 -x435 x436 -x437 x438 -x439 x440 x441 -x442 -x443 x444 -x445 -x446 -x447 -x448 -x449 x450 x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 x462 -x463 -x464 -x465 x466 x467 -x468 -x469 -x470 -x471 -x472 -x473 x474 -x475 -x476 -x477 -x478 x479 -x480 -x481 -x482 -x483 -x484 -x485 x486 x487 -x488 -x489 x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 x498 x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 x510 -x511 -x512 -x513 x514 x515 -x516 x517 -x518 -x519 -x520 -x521 x522 -x523 -x524 -x525 x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 x534 x535 -x536 -x537 -x538 -x539 -x540 -x541 x542 -x543 x544 -x545 x546 -x547 x548 x549 -x550 -x551 x552 -x553 -x554 x555 -x556 -x557 x558 -x559 -x560 -x561 x562 -x563 -x564 -x565 -x566 x567 -x568 -x569 x570 -x571 -x572 -x573 x574 -x575 -x576 -x577 x578 -x579 x580 -x581 x582 -x583 x584 x585 -x586 -x587 x588 -x589 -x590 -x591 -x592 -x593 x594 -x595 -x596 -x597 x598 x599 -x600 -x601 -x602 -x603 -x604 -x605 x606 x607 -x608 -x609 x610 -x611 -x612 -x613 x614 -x615 x616 -x617 x618 -x619 x620 x621 -x622 -x623 x624 x625 -x626 -x627 -x628 -x629 x630 -x631 -x632 -x633 x634 -x635 -x636 -x637 -x638 x639 -x640 -x641 x642 -x643 -x644 -x645 x646 -x647 -x648 -x649 x650 -x651 x652 -x653 x654 -x655 x656 x657 -x658 -x659 x660 -x661 -x662 -x663 -x664 -x665 x666 x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 x675 -x676 -x677 x678 x679 -x680 -x681 x682 -x683 -x684 -x685 x686 -x687 x688 -x689 x690 -x691 x692 x693 -x694 -x695 x696 -x697 x698 -x699 x700 -x701 x702 -x703 x704 x705 -x706 -x707 x708 -x709 x710 -x711 x712 -x713 x714 -x715 x716 x717 -x718 -x719 x720 -x721 x722 -x723 x724 -x725 x726 -x727 x728 x729 -x730 -x731 x732 -x733 -x734 -x735 -x736 -x737 x738 -x739 -x740 -x741 x742 x743 -x744 -x745 x746 -x747 x748 x749 -x750 -x751 x752 -x753 x754 -x755 x756 -x757 -x758 x759 -x760 -x761 x762 -x763 -x764 -x765 x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 x774 x775 -x776 -x777 x778 -x779 -x780 -x781 -x782 x783 -x784 -x785 x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 x794 -x795 x796 -x797 x798 -x799 x800 x801 -x802 -x803 x804 -x805 x806 -x807 x808 -x809 x810 -x811 x812 x813 -x814 -x815 x816 -x817 x818 -x819 x820 -x821 x822 -x823 x824 x825 -x826 -x827 x828 -x829 x830 -x831 x832 -x833 x834 -x835 x836 x837 -x838 -x839 x840 -x841 x842 -x843 x844 -x845 x846 -x847 x848 x849 -x850 -x851 x852 -x853 -x854 -x855 -x856 -x857 x858 x859 -x860 -x861 x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 x870 -x871 -x872 -x873 x874 x875 -x876 -x877 -x878 x879 -x880 -x881 -x882 -x883 -x884 -x885 x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 x894 -x895 -x896 x897 -x898 -x899 x900 -x901 x902 -x903 x904 -x905 x906 -x907 x908 x909 -x910 -x911 x912 x913 -x914 -x915 -x916 -x917 x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 x927 -x928 -x929 x930 x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 x942 x943 -x944 -x945 x946 -x947 x948 x949 -x950 -x951 -x952 -x953 x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 x962 -x963 x964 -x965 x966 -x967 x968 x969 -x970 -x971 x972 -x973 x974 -x975 x976 -x977 x978 -x979 x980 x981 -x982 -x983 x984 -x985 -x986 -x987 -x988 -x989 x990 -x991 -x992 -x993 -x994 x995 -x996 -x997 x998 -x999 x1000 -x1001 x1002 -x1003 x1004 x1005 -x1006 -x1007 x1008 -x1009 -x1010 x1011 -x1012 -x1013 x1014 -x1015 -x1016 -x1017 x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 x1026 x1027 -x1028 -x1029 x1030 -x1031 x1032 -x1033 -x1034 -x1035 x1036 -x1037 x1038 x1039 -x1040 -x1041 x1042 -x1043 -x1044 -x1045 -x1046 x1047 -x1048 -x1049 x1050 -x1051 x1052 -x1053 x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 x1062 x1063 -x1064 -x1065 x1066 -x1067 -x1068 -x1069 x1070 -x1071 x1072 -x1073 x1074 -x1075 x1076 x1077 -x1078 -x1079 x1080 -x1081 x1082 -x1083 x1084 -x1085 x1086 -x1087 x1088 x1089 -x1090 -x1091 x1092 -x1093 -x1094 -x1095 -x1096 -x1097 x1098 -x1099 -x1100 x1101 -x1102 -x1103 -x1104 x1105 -x1106 -x1107 -x1108 -x1109 x1110 -x1111 -x1112 -x1113 x1114 -x1115 -x1116 -x1117 x1118 -x1119 x1120 -x1121 x1122 -x1123 x1124 x1125 -x1126 -x1127 x1128 x1129 -x1130 -x1131 x1132 -x1133 x1134 x1135 -x1136 -x1137 x1138 x1139 -x1140 -x1141 x1142 -x1143 x1144 -x1145 x1146 -x1147 x1148 x1149 -x1150 -x1151 x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 x1159 -x1160 -x1161 x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 x1170 -x1171 x1172 x1173 -x1174 -x1175 x1176 x1177 -x1178 x1179 -x1180 -x1181 x1182 -x1183 x1184 -x1185 x1186 -x1187 x1188 -x1189 x1190 -x1191 x1192 -x1193 x1194 -x1195 x1196 x1197 -x1198 -x1199 x1200 x1201 -x1202 x1203 -x1204 -x1205 x1206 -x1207 x1208 -x1209 x1210 -x1211 x1212 -x1213 x1214 -x1215 x1216 -x1217 x1218 -x1219 x1220 x1221 -x1222 -x1223 x1224 -x1225 x1226 -x1227 x1228 -x1229 x1230 -x1231 x1232 x1233 -x1234 -x1235 x1236 x1237 -x1238 x1239 -x1240 -x1241 x1242 -x1243 x1244 x1245 -x1246 x1247 -x1248 x1249 -x1250 -x1251 -x1252 -x1253 x1254 -x1255 x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 x1263 -x1264 -x1265 x1266 -x1267 x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 x1278 x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 x1287 -x1288 -x1289 x1290 -x1291 -x1292 -x1293 x1294 -x1295 -x1296 -x1297 x1298 -x1299 x1300 -x1301 x1302 -x1303 x1304 x1305 -x1306 -x1307 x1308 -x1309 -x1310 -x1311 -x1312 -x1313 x1314 x1315 -x1316 -x1317 x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 x1326 -x1327 -x1328 -x1329 x1330 x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 x1338 x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 x1350 -x1351 -x1352 -x1353 x1354 x1355 -x1356 -x1357 -x1358 x1359 -x1360 -x1361 x1362 -x1363 x1364 -x1365 x1366 -x1367 x1368 -x1369 x1370 -x1371 x1372 -x1373 x1374 -x1375 x1376 x1377 -x1378 -x1379 x1380 -x1381 -x1382 x1383 -x1384 -x1385 x1386 -x1387 -x1388 -x1389 x1390 -x1391 -x1392 -x1#### 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.86 0.95 0.90 2/54 31948 Raw data (stat): 31948 (runsolver) R 31947 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481551069 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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 s] Raw data (loadavg): 0.88 0.95 0.90 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7113 0 0 0 981 16 0 0 25 0 1 0 481551069 33124352 6775 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8087 6775 603 41 0 8046 0 vsize: 32348 [startup+20.0004 s] Raw data (loadavg): 0.90 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7130 0 0 0 1981 16 0 0 25 0 1 0 481551069 33259520 6792 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8120 6792 603 41 0 8079 0 vsize: 32480 [startup+30.0007 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7155 0 0 0 2980 16 0 0 25 0 1 0 481551069 33406976 6817 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8156 6817 603 41 0 8115 0 vsize: 32624 [startup+40.0011 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7155 0 0 0 3980 17 0 0 25 0 1 0 481551069 33406976 6817 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8156 6817 603 41 0 8115 0 vsize: 32624 [startup+50.0015 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7203 0 0 0 4980 17 0 0 25 0 1 0 481551069 33542144 6865 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8189 6865 603 41 0 8148 0 vsize: 32756 [startup+60.0016 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7227 0 0 0 5980 17 0 0 25 0 1 0 481551069 33677312 6889 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8222 6889 603 41 0 8181 0 vsize: 32888 [startup+70.0023 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7245 0 0 0 6980 17 0 0 25 0 1 0 481551069 33677312 6907 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8222 6907 603 41 0 8181 0 vsize: 32888 [startup+80.0026 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7263 0 0 0 7981 17 0 0 25 0 1 0 481551069 33812480 6925 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8255 6925 603 41 0 8214 0 vsize: 33020 [startup+90.0037 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7300 0 0 0 8981 17 0 0 25 0 1 0 481551069 33947648 6962 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8288 6962 603 41 0 8247 0 vsize: 33152 [startup+100.004 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7363 0 0 0 9980 17 0 0 25 0 1 0 481551069 34217984 7025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8354 7025 603 41 0 8313 0 vsize: 33416 [startup+110.005 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7402 0 0 0 10980 17 0 0 25 0 1 0 481551069 34353152 7064 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8387 7064 603 41 0 8346 0 vsize: 33548 [startup+120.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7417 0 0 0 11980 18 0 0 25 0 1 0 481551069 34484224 7079 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8419 7079 603 41 0 8378 0 vsize: 33676 [startup+130.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7462 0 0 0 12981 18 0 0 25 0 1 0 481551069 34611200 7124 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8450 7124 603 41 0 8409 0 vsize: 33800 [startup+140.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7541 0 0 0 13981 18 0 0 25 0 1 0 481551069 34881536 7203 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8516 7203 603 41 0 8475 0 vsize: 34064 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7590 0 0 0 14981 18 0 0 25 0 1 0 481551069 35151872 7252 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8582 7252 603 41 0 8541 0 vsize: 34328 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7684 0 0 0 15981 18 0 0 25 0 1 0 481551069 35422208 7346 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8648 7346 603 41 0 8607 0 vsize: 34592 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7731 0 0 0 16981 19 0 0 25 0 1 0 481551069 35692544 7393 4294967295 134512640 134672761 3221224576 3221223648 134553549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8714 7393 603 41 0 8673 0 vsize: 34856 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7772 0 0 0 17980 19 0 0 25 0 1 0 481551069 35938304 7434 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8774 7434 603 41 0 8733 0 vsize: 35096 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7810 0 0 0 18980 19 0 0 25 0 1 0 481551069 36073472 7472 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8807 7472 603 41 0 8766 0 vsize: 35228 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7901 0 0 0 19980 20 0 0 25 0 1 0 481551069 36343808 7563 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8873 7563 603 41 0 8832 0 vsize: 35492 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 7990 0 0 0 20980 20 0 0 25 0 1 0 481551069 36741120 7652 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8970 7652 603 41 0 8929 0 vsize: 35880 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 8166 0 0 0 21979 21 0 0 25 0 1 0 481551069 37412864 7828 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9134 7828 603 41 0 9093 0 vsize: 36536 [startup+230.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 8643 0 0 0 22979 22 0 0 25 0 1 0 481551069 39555072 8305 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9657 8305 603 41 0 9616 0 vsize: 38628 [startup+240.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 8928 0 0 0 23978 23 0 0 25 0 1 0 481551069 40640512 8590 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9922 8590 603 41 0 9881 0 vsize: 39688 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31948 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9258 0 0 0 24977 23 0 0 25 0 1 0 481551069 42479616 8920 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10371 8920 603 41 0 10330 0 vsize: 41484 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9359 0 0 0 25977 23 0 0 25 0 1 0 481551069 42885120 9021 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10470 9021 603 41 0 10429 0 vsize: 41880 [startup+270.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9479 0 0 0 26977 24 0 0 25 0 1 0 481551069 43282432 9141 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10567 9141 603 41 0 10526 0 vsize: 42268 [startup+280.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9676 0 0 0 27977 25 0 0 25 0 1 0 481551069 44085248 9338 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10763 9338 603 41 0 10722 0 vsize: 43052 [startup+290.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9769 0 0 0 28976 25 0 0 25 0 1 0 481551069 44355584 9418 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10829 9418 603 41 0 10788 0 vsize: 43316 [startup+300.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9773 0 0 0 29976 25 0 0 25 0 1 0 481551069 44355584 9422 4294967295 134512640 134672761 3221224576 3221223728 134561040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10829 9422 603 41 0 10788 0 vsize: 43316 [startup+310.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9787 0 0 0 30976 25 0 0 25 0 1 0 481551069 44355584 9424 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10829 9424 603 41 0 10788 0 vsize: 43316 [startup+320.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9838 0 0 0 31977 25 0 0 25 0 1 0 481551069 44617728 9475 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10893 9475 603 41 0 10852 0 vsize: 43572 [startup+330.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 9991 0 0 0 32976 26 0 0 25 0 1 0 481551069 45281280 9628 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11055 9628 603 41 0 11014 0 vsize: 44220 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 10103 0 0 0 33976 26 0 0 25 0 1 0 481551069 45682688 9740 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11153 9740 603 41 0 11112 0 vsize: 44612 [startup+350.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 10234 0 0 0 34976 26 0 0 25 0 1 0 481551069 46014464 9838 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11234 9838 603 41 0 11193 0 vsize: 44936 [startup+360.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 10396 0 0 0 35976 27 0 0 25 0 1 0 481551069 46952448 10000 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11463 10000 603 41 0 11422 0 vsize: 45852 [startup+370.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 10512 0 0 0 36976 27 0 0 25 0 1 0 481551069 47493120 10116 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11595 10116 603 41 0 11554 0 vsize: 46380 [startup+380.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 10656 0 0 0 37976 27 0 0 25 0 1 0 481551069 48033792 10260 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11727 10260 603 41 0 11686 0 vsize: 46908 [startup+390.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 10896 0 0 0 38975 28 0 0 25 0 1 0 481551069 48975872 10500 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11957 10500 603 41 0 11916 0 vsize: 47828 [startup+400.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 39974 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+410.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 40974 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+420.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 41974 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+430.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 42974 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+440.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 43974 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+450.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 44974 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+460.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 45975 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+470.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 46975 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+480.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 47975 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+490.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 48975 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+500.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 49975 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+510.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 50975 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+520.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 51976 30 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+530.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 52976 31 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223680 134560361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+540.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 53976 31 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223744 134561256 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+550.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 54976 31 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223712 134565056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+560.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 55976 31 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+570.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11110 0 0 0 56976 31 0 0 25 0 1 0 481551069 49684480 10681 4294967295 134512640 134672761 3221224576 3221223680 134560059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12130 10681 603 41 0 12089 0 vsize: 48520 [startup+580.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11294 0 0 0 57976 31 0 0 25 0 1 0 481551069 50475008 10865 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12323 10865 603 41 0 12282 0 vsize: 49292 [startup+590.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11540 0 0 0 58976 32 0 0 25 0 1 0 481551069 51548160 11111 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12585 11111 603 41 0 12544 0 vsize: 50340 [startup+600.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 11842 0 0 0 59975 33 0 0 25 0 1 0 481551069 52756480 11413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12880 11413 603 41 0 12839 0 vsize: 51520 [startup+610.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 12063 0 0 0 60974 34 0 0 25 0 1 0 481551069 53686272 11634 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13107 11634 603 41 0 13066 0 vsize: 52428 [startup+620.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 12259 0 0 0 61974 34 0 0 25 0 1 0 481551069 54489088 11830 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13303 11830 603 41 0 13262 0 vsize: 53212 [startup+630.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 12466 0 0 0 62972 36 0 0 25 0 1 0 481551069 55279616 12037 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13496 12037 603 41 0 13455 0 vsize: 53984 [startup+640.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 12696 0 0 0 63972 37 0 0 25 0 1 0 481551069 56197120 12267 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13720 12267 603 41 0 13679 0 vsize: 54880 [startup+650.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 12877 0 0 0 64971 38 0 0 25 0 1 0 481551069 56987648 12448 4294967295 134512640 134672761 3221224576 3221223712 134565149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13913 12448 603 41 0 13872 0 vsize: 55652 [startup+660.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 13056 0 0 0 65970 39 0 0 25 0 1 0 481551069 57651200 12627 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14075 12627 603 41 0 14034 0 vsize: 56300 [startup+670.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 13323 0 0 0 66969 40 0 0 25 0 1 0 481551069 58863616 12894 4294967295 134512640 134672761 3221224576 3221223592 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14371 12894 603 41 0 14330 0 vsize: 57484 [startup+680.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 13458 0 0 0 67969 40 0 0 25 0 1 0 481551069 59392000 13029 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14500 13030 603 41 0 14459 0 vsize: 58000 [startup+690.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 13729 0 0 0 68968 42 0 0 25 0 1 0 481551069 60465152 13300 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14762 13300 603 41 0 14721 0 vsize: 59048 [startup+700.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14029 0 0 0 69967 43 0 0 25 0 1 0 481551069 61669376 13600 4294967295 134512640 134672761 3221224576 3221223760 134559381 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15056 13601 603 41 0 15015 0 vsize: 60224 [startup+710.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14300 0 0 0 70966 44 0 0 25 0 1 0 481551069 62734336 13871 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15316 13871 603 41 0 15275 0 vsize: 61264 [startup+720.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14667 0 0 0 71965 45 0 0 25 0 1 0 481551069 64049152 14204 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14204 603 41 0 15596 0 vsize: 62548 [startup+730.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14667 0 0 0 72965 45 0 0 25 0 1 0 481551069 64049152 14204 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14204 603 41 0 15596 0 vsize: 62548 [startup+740.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14667 0 0 0 73965 45 0 0 25 0 1 0 481551069 64049152 14204 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14204 603 41 0 15596 0 vsize: 62548 [startup+750.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14667 0 0 0 74965 45 0 0 25 0 1 0 481551069 64049152 14204 4294967295 134512640 134672761 3221224576 3221223728 134565101 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14204 603 41 0 15596 0 vsize: 62548 [startup+760.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 75965 45 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+770.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 76966 45 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+780.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 77966 45 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+790.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 78966 45 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+800.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 79966 46 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223744 134561266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+810.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 80966 46 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+820.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 81966 46 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+830.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 82966 46 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+840.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14668 0 0 0 83966 46 0 0 25 0 1 0 481551069 64049152 14205 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14205 603 41 0 15596 0 vsize: 62548 [startup+850.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 84967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+860.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 85967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+870.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 86967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+880.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 87967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223728 134564780 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+890.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 88967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+900.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 89967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+910.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 90967 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+920.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 91969 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+930.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 92977 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223680 134560393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+940.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 93977 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+950.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 94977 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+960.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 95977 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+970.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 96977 46 0 0 25 0 1 0 481551069 64049152 14207 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15637 14207 603 41 0 15596 0 vsize: 62548 [startup+980.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 97978 46 0 0 25 0 1 0 481551069 64045056 14206 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14206 603 41 0 15595 0 vsize: 62544 [startup+990.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 98978 46 0 0 25 0 1 0 481551069 64045056 14206 4294967295 134512640 134672761 3221224576 3221223680 134554912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14206 603 41 0 15595 0 vsize: 62544 [startup+1000.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14670 0 0 0 99978 47 0 0 25 0 1 0 481551069 64045056 14206 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14206 603 41 0 15595 0 vsize: 62544 [startup+1010.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 100978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1020.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 101978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1030.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 102978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1040.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 103978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1050.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 104978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1060.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 105978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1070.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 106978 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1080.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 107979 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1090.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 108979 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1100.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 109979 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 110979 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 111979 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 112979 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 113980 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 114980 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 115980 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14671 0 0 0 116980 47 0 0 25 0 1 0 481551069 64045056 14207 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14207 603 41 0 15595 0 vsize: 62544 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14672 0 0 0 117980 47 0 0 25 0 1 0 481551069 64045056 14208 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14208 603 41 0 15595 0 vsize: 62544 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14672 0 0 0 118980 48 0 0 25 0 1 0 481551069 64045056 14208 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14208 603 41 0 15595 0 vsize: 62544 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31950 Raw data (stat): 31948 (minisat+) R 31947 26298 26297 0 -1 0 14672 0 0 0 119980 48 0 0 25 0 1 0 481551069 64045056 14208 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15636 14208 603 41 0 15595 0 vsize: 62544 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.15 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 31950 Raw data (stat): 31948 (minisat+) Z 31947 26298 26297 0 -1 12 14675 0 0 0 119980 50 0 0 25 0 1 0 481551069 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.15 CPU time (s): 1200.32 CPU user time (s): 1199.81 CPU system time (s): 0.508922 CPU usage (%): 100.014 Max. virtual memory (Kb): 62548 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####