Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core2586-950.opb |
MD5SUM | d227b04d1ac4226bb8116c410fa055ae |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2147483647 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 13435 |
Biggest coefficient in the objective function | 52428800000000000 |
Number of bits for the biggest coefficient in the objective function | 56 |
Sum of the numbers in the objective function | 224301741012582900 |
Number of bits of the sum of numbers in the objective function | 58 |
Biggest number in a constraint | 1280000000000000000000 |
Number of bits of the biggest number in a constraint | 71 |
Biggest sum of numbers in a constraint | 1280224301741012680704 |
Number of bits of the biggest sum of numbers | 71 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 10.8873 |
Number of variables | 13435 |
Total number of constraints | 15804 |
Number of constraints which are clauses | 2586 |
Number of constraints which are cardinality constraints (but not clauses) | 13217 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 13435 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-04-20 22:22:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=20042 boxname=wulflinc29 idbench=1542 idsolver=9 numberseed=0 MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac /oldhome/oroussel/solvers/sat4jPseudo.jar MD5SUM BENCH: d227b04d1ac4226bb8116c410fa055ae /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-core2586-950.opb REAL COMMAND: java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-core2586-950.opb IDLAUNCH: 20042 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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: 358192 kB Buffers: 37340 kB Cached: 598244 kB SwapCached: 12 kB Active: 198212 kB Inactive: 440236 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 357940 kB SwapTotal: 2097892 kB SwapFree: 2097880 kB Dirty: 36 kB Writeback: 0 kB Mapped: 6944 kB Slab: 32448 kB Committed_AS: 63492 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 22:45:41 (client local time) WITH STATUS 1 IN 1377.64 SECONDS stats: 20042 7 1377.64 1 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c solving /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-core2586-950.opb c reading problem c [nbvar=13435] c [nbconstr=15804] c time 61.725 c #vars 13435 c #clauses 2589 c starts : 0 c conflicts : 0 c decisions : 0 c propagations : 0 c inspects : 0 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 0 c SATISFIABLE c OPTIMIZING... c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 63.889 c starts : 1 c conflicts : 0 c decisions : 12664 c propagations : 13435 c inspects : 19499 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 1 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 64.21 c starts : 2 c conflicts : 0 c decisions : 25328 c propagations : 26838 c inspects : 21460 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 2 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 64.486 c starts : 3 c conflicts : 0 c decisions : 37992 c propagations : 40241 c inspects : 23063 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 3 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 65.055 c starts : 4 c conflicts : 0 c decisions : 50656 c propagations : 53644 c inspects : 24693 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 4 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 65.336 c starts : 5 c conflicts : 0 c decisions : 63320 c propagations : 67047 c inspects : 26289 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 5 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 65.637 c starts : 6 c conflicts : 0 c decisions : 75984 c propagations : 80450 c inspects : 27919 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 6 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 65.945 c starts : 7 c conflicts : 0 c decisions : 88648 c propagations : 93853 c inspects : 29549 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 7 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 66.249 c starts : 8 c conflicts : 0 c decisions : 101312 c propagations : 107256 c inspects : 31179 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 8 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 66.536 c starts : 9 c conflicts : 0 c decisions : 113976 c propagations : 120659 c inspects : 32783 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 9 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 67.126 c starts : 10 c conflicts : 0 c decisions : 126640 c propagations : 134062 c inspects : 34413 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 10 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 67.434 c starts : 11 c conflicts : 0 c decisions : 139304 c propagations : 147465 c inspects : 36043 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 11 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 67.719 c starts : 12 c conflicts : 0 c decisions : 151968 c propagations : 160868 c inspects : 37647 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 12 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 68.036 c starts : 13 c conflicts : 0 c decisions : 164632 c propagations : 174271 c inspects : 39277 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 13 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 68.345 c starts : 14 c conflicts : 0 c decisions : 177296 c propagations : 187674 c inspects : 40907 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 14 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 69.019 c starts : 15 c conflicts : 0 c decisions : 189960 c propagations : 201077 c inspects : 42537 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 15 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 69.315 c starts : 16 c conflicts : 0 c decisions : 202624 c propagations : 214480 c inspects : 44144 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 16 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 69.62 c starts : 17 c conflicts : 0 c decisions : 215288 c propagations : 227883 c inspects : 45730 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 17 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 69.942 c starts : 18 c conflicts : 0 c decisions : 227952 c propagations : 241286 c inspects : 47360 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 18 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 70.242 c starts : 19 c conflicts : 0 c decisions : 240616 c propagations : 254689 c inspects : 48962 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 19 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 70.567 c starts : 20 c conflicts : 0 c decisions : 253280 c propagations : 268092 c inspects : 50592 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 20 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 70.872 c starts : 21 c conflicts : 0 c decisions : 265944 c propagations : 281495 c inspects : 52194 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 21 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 71.571 c starts : 22 c conflicts : 0 c decisions : 278608 c propagations : 294898 c inspects : 53824 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 22 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 71.917 c starts : 23 c conflicts : 0 c decisions : 291272 c propagations : 308301 c inspects : 55454 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 23 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 72.251 c starts : 24 c conflicts : 0 c decisions : 303936 c propagations : 321704 c inspects : 57084 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 24 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 72.589 c starts : 25 c conflicts : 0 c decisions : 316600 c propagations : 335107 c inspects : 58714 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 25 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 72.902 c starts : 26 c conflicts : 0 c decisions : 329264 c propagations : 348510 c inspects : 60307 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 26 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 73.6 c starts : 27 c conflicts : 0 c decisions : 341928 c propagations : 361913 c inspects : 61937 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 27 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 73.944 c starts : 28 c conflicts : 0 c decisions : 354592 c propagations : 375316 c inspects : 63567 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 28 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 74.264 c starts : 29 c conflicts : 0 c decisions : 367256 c propagations : 388719 c inspects : 65171 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 29 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 74.611 c starts : 30 c conflicts : 0 c decisions : 379920 c propagations : 402122 c inspects : 66801 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 30 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 74.961 c starts : 31 c conflicts : 0 c decisions : 392584 c propagations : 415525 c inspects : 68431 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 31 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 75.312 c starts : 32 c conflicts : 0 c decisions : 405248 c propagations : 428928 c inspects : 70061 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 32 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 76.056 c starts : 33 c conflicts : 0 c decisions : 417912 c propagations : 442331 c inspects : 71691 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 33 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 76.385 c starts : 34 c conflicts : 0 c decisions : 430576 c propagations : 455734 c inspects : 73294 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 34 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 76.743 c starts : 35 c conflicts : 0 c decisions : 443240 c propagations : 469137 c inspects : 74924 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 35 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 77.102 c starts : 36 c conflicts : 0 c decisions : 455904 c propagations : 482540 c inspects : 76554 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 36 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 77.462 c starts : 37 c conflicts : 0 c decisions : 468568 c propagations : 495943 c inspects : 78184 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 37 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 77.825 c starts : 38 c conflicts : 0 c decisions : 481232 c propagations : 509346 c inspects : 79814 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 38 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 78.516 c starts : 39 c conflicts : 0 c decisions : 493896 c propagations : 522749 c inspects : 81444 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 39 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 78.884 c starts : 40 c conflicts : 0 c decisions : 506560 c propagations : 536152 c inspects : 83074 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 40 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 79.253 c starts : 41 c conflicts : 0 c decisions : 519224 c propagations : 549555 c inspects : 84704 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 41 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 79.63 c starts : 42 c conflicts : 0 c decisions : 531888 c propagations : 562958 c inspects : 86334 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 42 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 79.989 c starts : 43 c conflicts : 0 c decisions : 544552 c propagations : 576361 c inspects : 87929 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 43 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 80.365 c starts : 44 c conflicts : 0 c decisions : 557216 c propagations : 589764 c inspects : 89559 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 44 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 81.085 c starts : 45 c conflicts : 0 c decisions : 569880 c propagations : 603167 c inspects : 91189 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 45 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 81.462 c starts : 46 c conflicts : 0 c decisions : 582544 c propagations : 616570 c inspects : 92819 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 46 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 81.839 c starts : 47 c conflicts : 0 c decisions : 595208 c propagations : 629973 c inspects : 94449 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 47 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 82.22 c starts : 48 c conflicts : 0 c decisions : 607872 c propagations : 643376 c inspects : 96079 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 48 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 82.601 c starts : 49 c conflicts : 0 c decisions : 620536 c propagations : 656779 c inspects : 97709 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 49 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 83.343 c starts : 50 c conflicts : 0 c decisions : 633200 c propagations : 670182 c inspects : 99339 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 50 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 83.737 c starts : 51 c conflicts : 0 c decisions : 645864 c propagations : 683585 c inspects : 100969 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 51 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 84.132 c starts : 52 c conflicts : 0 c decisions : 658528 c propagations : 696988 c inspects : 102599 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 52 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 84.505 c starts : 53 c conflicts : 0 c decisions : 671192 c propagations : 710391 c inspects : 104203 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 53 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 84.878 c starts : 54 c conflicts : 0 c decisions : 683856 c propagations : 723794 c inspects : 105805 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 54 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 85.278 c starts : 55 c conflicts : 0 c decisions : 696520 c propagations : 737197 c inspects : 107435 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 55 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 86.038 c starts : 56 c conflicts : 0 c decisions : 709184 c propagations : 750600 c inspects : 109065 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 56 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 86.443 c starts : 57 c conflicts : 0 c decisions : 721848 c propagations : 764003 c inspects : 110695 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 57 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 86.849 c starts : 58 c conflicts : 0 c decisions : 734512 c propagations : 777406 c inspects : 112325 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 58 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 87.261 c starts : 59 c conflicts : 0 c decisions : 747176 c propagations : 790809 c inspects : 113955 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 59 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 87.673 c starts : 60 c conflicts : 0 c decisions : 759840 c propagations : 804212 c inspects : 115585 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 60 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 88.063 c starts : 61 c conflicts : 0 c decisions : 772504 c propagations : 817615 c inspects : 117189 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 61 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 88.82 c starts : 62 c conflicts : 0 c decisions : 785168 c propagations : 831018 c inspects : 118797 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 62 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 89.237 c starts : 63 c conflicts : 0 c decisions : 797832 c propagations : 844421 c inspects : 120427 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 63 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 89.655 c starts : 64 c conflicts : 0 c decisions : 810496 c propagations : 857824 c inspects : 122057 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 64 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 90.13 c starts : 65 c conflicts : 0 c decisions : 823160 c propagations : 871227 c inspects : 123687 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 65 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 90.555 c starts : 66 c conflicts : 0 c decisions : 835824 c propagations : 884630 c inspects : 125317 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 66 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 91.406 c starts : 67 c conflicts : 0 c decisions : 848488 c propagations : 898033 c inspects : 126947 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 67 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 91.835 c starts : 68 c conflicts : 0 c decisions : 861152 c propagations : 911436 c inspects : 128577 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 68 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 92.241 c starts : 69 c conflicts : 0 c decisions : 873816 c propagations : 924839 c inspects : 130179 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 69 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 92.646 c starts : 70 c conflicts : 0 c decisions : 886480 c propagations : 938242 c inspects : 131783 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 70 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 93.075 c starts : 71 c conflicts : 0 c decisions : 899144 c propagations : 951645 c inspects : 133413 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 71 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 93.506 c starts : 72 c conflicts : 0 c decisions : 911808 c propagations : 965048 c inspects : 135043 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 72 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 94.212 c starts : 73 c conflicts : 0 c decisions : 924472 c propagations : 978451 c inspects : 136673 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 73 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 94.653 c starts : 74 c conflicts : 0 c decisions : 937136 c propagations : 991854 c inspects : 138303 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 74 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 95.07 c starts : 75 c conflicts : 0 c decisions : 949800 c propagations : 1005257 c inspects : 139896 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 75 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 95.514 c starts : 76 c conflicts : 0 c decisions : 962464 c propagations : 1018660 c inspects : 141526 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 76 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 95.96 c starts : 77 c conflicts : 0 c decisions : 975128 c propagations : 1032063 c inspects : 143156 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 77 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 96.411 c starts : 78 c conflicts : 0 c decisions : 987792 c propagations : 1045466 c inspects : 144786 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 78 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 97.197 c starts : 79 c conflicts : 0 c decisions : 1000456 c propagations : 1058869 c inspects : 146416 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 79 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 97.651 c starts : 80 c conflicts : 0 c decisions : 1013120 c propagations : 1072272 c inspects : 148046 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 80 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 98.106 c starts : 81 c conflicts : 0 c decisions : 1025784 c propagations : 1085675 c inspects : 149676 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 81 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 98.565 c starts : 82 c conflicts : 0 c decisions : 1038448 c propagations : 1099078 c inspects : 151306 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 82 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 99.026 c starts : 83 c conflicts : 0 c decisions : 1051112 c propagations : 1112481 c inspects : 152936 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 83 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 99.465 c starts : 84 c conflicts : 0 c decisions : 1063776 c propagations : 1125884 c inspects : 154540 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 84 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 100.263 c starts : 85 c conflicts : 0 c decisions : 1076440 c propagations : 1139287 c inspects : 156170 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 85 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 100.712 c starts : 86 c conflicts : 0 c decisions : 1089104 c propagations : 1152690 c inspects : 157776 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 86 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 101.181 c starts : 87 c conflicts : 0 c decisions : 1101768 c propagations : 1166093 c inspects : 159406 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 87 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 101.651 c starts : 88 c conflicts : 0 c decisions : 1114432 c propagations : 1179496 c inspects : 161036 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 88 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 102.124 c starts : 89 c conflicts : 0 c decisions : 1127096 c propagations : 1192899 c inspects : 162666 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 89 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 102.602 c starts : 90 c conflicts : 0 c decisions : 1139760 c propagations : 1206302 c inspects : 164296 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 90 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 103.401 c starts : 91 c conflicts : 0 c decisions : 1152424 c propagations : 1219705 c inspects : 165893 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 91 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 103.882 c starts : 92 c conflicts : 0 c decisions : 1165088 c propagations : 1233108 c inspects : 167523 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 92 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 104.363 c starts : 93 c conflicts : 0 c decisions : 1177752 c propagations : 1246511 c inspects : 169153 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 93 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 104.848 c starts : 94 c conflicts : 0 c decisions : 1190416 c propagations : 1259914 c inspects : 170783 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 94 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 105.309 c starts : 95 c conflicts : 0 c decisions : 1203080 c propagations : 1273317 c inspects : 172387 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 95 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 105.798 c starts : 96 c conflicts : 0 c decisions : 1215744 c propagations : 1286720 c inspects : 174017 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 96 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 106.641 c starts : 97 c conflicts : 0 c decisions : 1228408 c propagations : 1300123 c inspects : 175647 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 97 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 107.115 c starts : 98 c conflicts : 0 c decisions : 1241072 c propagations : 1313526 c inspects : 177240 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 98 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 107.616 c starts : 99 c conflicts : 0 c decisions : 1253736 c propagations : 1326929 c inspects : 178870 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 99 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 108.091 c starts : 100 c conflicts : 0 c decisions : 1266400 c propagations : 1340332 c inspects : 180455 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 100 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 108.567 c starts : 101 c conflicts : 0 c decisions : 1279064 c propagations : 1353735 c inspects : 182059 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 101 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 109.039 c starts : 102 c conflicts : 0 c decisions : 1291728 c propagations : 1367138 c inspects : 183646 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 102 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 109.912 c starts : 103 c conflicts : 0 c decisions : 1304392 c propagations : 1380541 c inspects : 185276 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 103 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 110.419 c starts : 104 c conflicts : 0 c decisions : 1317056 c propagations : 1393944 c inspects : 186906 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 104 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 110.928 c starts : 105 c conflicts : 0 c decisions : 1329720 c propagations : 1407347 c inspects : 188536 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 105 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 111.414 c starts : 106 c conflicts : 0 c decisions : 1342384 c propagations : 1420750 c inspects : 190140 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 106 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 111.925 c starts : 107 c conflicts : 0 c decisions : 1355048 c propagations : 1434153 c inspects : 191770 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 107 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 112.796 c starts : 108 c conflicts : 0 c decisions : 1367712 c propagations : 1447556 c inspects : 193400 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 108 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 113.311 c starts : 109 c conflicts : 0 c decisions : 1380376 c propagations : 1460959 c inspects : 195030 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 109 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 113.829 c starts : 110 c conflicts : 0 c decisions : 1393040 c propagations : 1474362 c inspects : 196660 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 110 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 114.351 c starts : 111 c conflicts : 0 c decisions : 1405704 c propagations : 1487765 c inspects : 198290 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 111 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 114.872 c starts : 112 c conflicts : 0 c decisions : 1418368 c propagations : 1501168 c inspects : 199920 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 112 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 115.397 c starts : 113 c conflicts : 0 c decisions : 1431032 c propagations : 1514571 c inspects : 201550 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 113 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 116.253 c starts : 114 c conflicts : 0 c decisions : 1443696 c propagations : 1527974 c inspects : 203180 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 114 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 116.776 c starts : 115 c conflicts : 0 c decisions : 1456360 c propagations : 1541377 c inspects : 204810 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 115 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 117.301 c starts : 116 c conflicts : 0 c decisions : 1469024 c propagations : 1554780 c inspects : 206440 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 116 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 117.83 c starts : 117 c conflicts : 0 c decisions : 1481688 c propagations : 1568183 c inspects : 208070 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 117 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 118.359 c starts : 118 c conflicts : 0 c decisions : 1494352 c propagations : 1581586 c inspects : 209700 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 118 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 118.891 c starts : 119 c conflicts : 0 c decisions : 1507016 c propagations : 1594989 c inspects : 211330 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 119 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 119.748 c starts : 120 c conflicts : 0 c decisions : 1519680 c propagations : 1608392 c inspects : 212960 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 120 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 120.285 c starts : 121 c conflicts : 0 c decisions : 1532344 c propagations : 1621795 c inspects : 214590 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 121 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 120.825 c starts : 122 c conflicts : 0 c decisions : 1545008 c propagations : 1635198 c inspects : 216220 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 122 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 121.365 c starts : 123 c conflicts : 0 c decisions : 1557672 c propagations : 1648601 c inspects : 217850 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 123 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 121.908 c starts : 124 c conflicts : 0 c decisions : 1570336 c propagations : 1662004 c inspects : 219480 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 124 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 122.799 c starts : 125 c conflicts : 0 c decisions : 1583000 c propagations : 1675407 c inspects : 221110 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 125 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 123.346 c starts : 126 c conflicts : 0 c decisions : 1595664 c propagations : 1688810 c inspects : 222740 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 126 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 123.871 c starts : 127 c conflicts : 0 c decisions : 1608328 c propagations : 1702213 c inspects : 224342 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 127 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 124.422 c starts : 128 c conflicts : 0 c decisions : 1620992 c propagations : 1715616 c inspects : 225972 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 128 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 125.089 c starts : 129 c conflicts : 0 c decisions : 1633656 c propagations : 1729019 c inspects : 227602 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 129 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 126.055 c starts : 130 c conflicts : 0 c decisions : 1646320 c propagations : 1742422 c inspects : 229232 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 130 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 126.613 c starts : 131 c conflicts : 0 c decisions : 1658984 c propagations : 1755825 c inspects : 230862 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 131 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 127.175 c starts : 132 c conflicts : 0 c decisions : 1671648 c propagations : 1769228 c inspects : 232492 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 132 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 127.715 c starts : 133 c conflicts : 0 c decisions : 1684312 c propagations : 1782631 c inspects : 234095 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 133 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 128.257 c starts : 134 c conflicts : 0 c decisions : 1696976 c propagations : 1796034 c inspects : 235699 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 134 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 128.823 c starts : 135 c conflicts : 0 c decisions : 1709640 c propagations : 1809437 c inspects : 237329 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 135 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 129.708 c starts : 136 c conflicts : 0 c decisions : 1722304 c propagations : 1822840 c inspects : 238959 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 136 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 130.277 c starts : 137 c conflicts : 0 c decisions : 1734968 c propagations : 1836243 c inspects : 240589 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 137 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 130.851 c starts : 138 c conflicts : 0 c decisions : 1747632 c propagations : 1849646 c inspects : 242219 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 138 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 131.433 c starts : 139 c conflicts : 0 c decisions : 1760296 c propagations : 1863049 c inspects : 243849 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 139 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 132.016 c starts : 140 c conflicts : 0 c decisions : 1772960 c propagations : 1876452 c inspects : 245479 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 140 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 132.956 c starts : 141 c conflicts : 0 c decisions : 1785624 c propagations : 1889855 c inspects : 247109 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 141 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 133.514 c starts : 142 c conflicts : 0 c decisions : 1798288 c propagations : 1903258 c inspects : 248710 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 142 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 134.098 c starts : 143 c conflicts : 0 c decisions : 1810952 c propagations : 1916661 c inspects : 250340 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 143 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 134.683 c starts : 144 c conflicts : 0 c decisions : 1823616 c propagations : 1930064 c inspects : 251970 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 144 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 135.271 c starts : 145 c conflicts : 0 c decisions : 1836280 c propagations : 1943467 c inspects : 253600 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 145 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 135.862 c starts : 146 c conflicts : 0 c decisions : 1848944 c propagations : 1956870 c inspects : 255230 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 146 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 136.769 c starts : 147 c conflicts : 0 c decisions : 1861608 c propagations : 1970273 c inspects : 256834 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 147 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 137.342 c starts : 148 c conflicts : 0 c decisions : 1874272 c propagations : 1983676 c inspects : 258436 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 148 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 137.943 c starts : 149 c conflicts : 0 c decisions : 1886936 c propagations : 1997079 c inspects : 260066 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 149 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 138.546 c starts : 150 c conflicts : 0 c decisions : 1899600 c propagations : 2010482 c inspects : 261696 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 150 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 139.152 c starts : 151 c conflicts : 0 c decisions : 1912264 c propagations : 2023885 c inspects : 263326 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 151 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 139.759 c starts : 152 c conflicts : 0 c decisions : 1924928 c propagations : 2037288 c inspects : 264956 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 152 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 140.706 c starts : 153 c conflicts : 0 c decisions : 1937592 c propagations : 2050691 c inspects : 266586 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 153 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 141.312 c starts : 154 c conflicts : 0 c decisions : 1950256 c propagations : 2064094 c inspects : 268216 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 154 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 141.924 c starts : 155 c conflicts : 0 c decisions : 1962920 c propagations : 2077497 c inspects : 269846 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 155 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 142.513 c starts : 156 c conflicts : 0 c decisions : 1975584 c propagations : 2090900 c inspects : 271452 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 156 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 143.132 c starts : 157 c conflicts : 0 c decisions : 1988248 c propagations : 2104303 c inspects : 273082 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 157 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 143.723 c starts : 158 c conflicts : 0 c decisions : 2000912 c propagations : 2117706 c inspects : 274684 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 158 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 144.679 c starts : 159 c conflicts : 0 c decisions : 2013576 c propagations : 2131109 c inspects : 276314 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 159 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 145.298 c starts : 160 c conflicts : 0 c decisions : 2026240 c propagations : 2144512 c inspects : 277944 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 160 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 145.921 c starts : 161 c conflicts : 0 c decisions : 2038904 c propagations : 2157915 c inspects : 279574 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 161 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 146.546 c starts : 162 c conflicts : 0 c decisions : 2051568 c propagations : 2171318 c inspects : 281204 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 162 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 147.145 c starts : 163 c conflicts : 0 c decisions : 2064232 c propagations : 2184721 c inspects : 282789 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 163 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 148.127 c starts : 164 c conflicts : 0 c decisions : 2076896 c propagations : 2198124 c inspects : 284419 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 164 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 148.762 c starts : 165 c conflicts : 0 c decisions : 2089560 c propagations : 2211527 c inspects : 286049 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 165 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 149.402 c starts : 166 c conflicts : 0 c decisions : 2102224 c propagations : 2224930 c inspects : 287679 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 166 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 150.037 c starts : 167 c conflicts : 0 c decisions : 2114888 c propagations : 2238333 c inspects : 289309 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 167 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 150.648 c starts : 168 c conflicts : 0 c decisions : 2127552 c propagations : 2251736 c inspects : 290902 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 168 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 151.291 c starts : 169 c conflicts : 0 c decisions : 2140216 c propagations : 2265139 c inspects : 292532 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 169 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 152.249 c starts : 170 c conflicts : 0 c decisions : 2152880 c propagations : 2278542 c inspects : 294129 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 170 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 152.892 c starts : 171 c conflicts : 0 c decisions : 2165544 c propagations : 2291945 c inspects : 295759 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 171 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 153.538 c starts : 172 c conflicts : 0 c decisions : 2178208 c propagations : 2305348 c inspects : 297389 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 172 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 154.185 c starts : 173 c conflicts : 0 c decisions : 2190872 c propagations : 2318751 c inspects : 299019 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 173 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 154.834 c starts : 174 c conflicts : 0 c decisions : 2203536 c propagations : 2332154 c inspects : 300649 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 174 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 155.49 c starts : 175 c conflicts : 0 c decisions : 2216200 c propagations : 2345557 c inspects : 302279 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 175 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 156.475 c starts : 176 c conflicts : 0 c decisions : 2228864 c propagations : 2358960 c inspects : 303909 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 176 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 157.13 c starts : 177 c conflicts : 0 c decisions : 2241528 c propagations : 2372363 c inspects : 305539 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 177 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 157.79 c starts : 178 c conflicts : 0 c decisions : 2254192 c propagations : 2385766 c inspects : 307169 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 178 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 158.422 c starts : 179 c conflicts : 0 c decisions : 2266856 c propagations : 2399169 c inspects : 308756 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 179 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 159.084 c starts : 180 c conflicts : 0 c decisions : 2279520 c propagations : 2412572 c inspects : 310386 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 180 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 159.749 c starts : 181 c conflicts : 0 c decisions : 2292184 c propagations : 2425975 c inspects : 312016 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 181 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 160.762 c starts : 182 c conflicts : 0 c decisions : 2304848 c propagations : 2439378 c inspects : 313646 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 182 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 161.44 c starts : 183 c conflicts : 0 c decisions : 2317512 c propagations : 2452781 c inspects : 315276 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 183 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 162.116 c starts : 184 c conflicts : 0 c decisions : 2330176 c propagations : 2466184 c inspects : 316906 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 184 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 162.795 c starts : 185 c conflicts : 0 c decisions : 2342840 c propagations : 2479587 c inspects : 318536 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 185 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 163.45 c starts : 186 c conflicts : 0 c decisions : 2355504 c propagations : 2492990 c inspects : 320138 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 186 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 164.489 c starts : 187 c conflicts : 0 c decisions : 2368168 c propagations : 2506393 c inspects : 321768 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 187 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 165.168 c starts : 188 c conflicts : 0 c decisions : 2380832 c propagations : 2519796 c inspects : 323398 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 188 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 165.852 c starts : 189 c conflicts : 0 c decisions : 2393496 c propagations : 2533199 c inspects : 325028 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 189 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 166.513 c starts : 190 c conflicts : 0 c decisions : 2406160 c propagations : 2546602 c inspects : 326637 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 190 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 167.203 c starts : 191 c conflicts : 0 c decisions : 2418824 c propagations : 2560005 c inspects : 328267 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 191 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 167.892 c starts : 192 c conflicts : 0 c decisions : 2431488 c propagations : 2573408 c inspects : 329897 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 192 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 168.909 c starts : 193 c conflicts : 0 c decisions : 2444152 c propagations : 2586811 c inspects : 331527 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 193 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 169.597 c starts : 194 c conflicts : 0 c decisions : 2456816 c propagations : 2600214 c inspects : 333129 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 194 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 170.272 c starts : 195 c conflicts : 0 c decisions : 2469480 c propagations : 2613617 c inspects : 334734 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 195 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 170.968 c starts : 196 c conflicts : 0 c decisions : 2482144 c propagations : 2627020 c inspects : 336364 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 196 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 171.67 c starts : 197 c conflicts : 0 c decisions : 2494808 c propagations : 2640423 c inspects : 337994 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 197 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 172.376 c starts : 198 c conflicts : 0 c decisions : 2507472 c propagations : 2653826 c inspects : 339624 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 198 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 173.457 c starts : 199 c conflicts : 0 c decisions : 2520136 c propagations : 2667229 c inspects : 341254 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 199 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 174.167 c starts : 200 c conflicts : 0 c decisions : 2532800 c propagations : 2680632 c inspects : 342884 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 200 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 174.88 c starts : 201 c conflicts : 0 c decisions : 2545464 c propagations : 2694035 c inspects : 344514 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 201 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 175.595 c starts : 202 c conflicts : 0 c decisions : 2558128 c propagations : 2707438 c inspects : 346144 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 202 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 176.312 c starts : 203 c conflicts : 0 c decisions : 2570792 c propagations : 2720841 c inspects : 347774 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 203 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 177.367 c starts : 204 c conflicts : 0 c decisions : 2583456 c propagations : 2734244 c inspects : 349404 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 204 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 178.082 c starts : 205 c conflicts : 0 c decisions : 2596120 c propagations : 2747647 c inspects : 351034 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 205 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 178.801 c starts : 206 c conflicts : 0 c decisions : 2608784 c propagations : 2761050 c inspects : 352664 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 206 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 179.506 c starts : 207 c conflicts : 0 c decisions : 2621448 c propagations : 2774453 c inspects : 354267 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 207 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 180.233 c starts : 208 c conflicts : 0 c decisions : 2634112 c propagations : 2787856 c inspects : 355897 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 208 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 180.98 c starts : 209 c conflicts : 0 c decisions : 2646776 c propagations : 2801259 c inspects : 357527 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 209 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 182.04 c starts : 210 c conflicts : 0 c decisions : 2659440 c propagations : 2814662 c inspects : 359157 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 210 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 182.77 c starts : 211 c conflicts : 0 c decisions : 2672104 c propagations : 2828065 c inspects : 360787 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 211 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 183.5 c starts : 212 c conflicts : 0 c decisions : 2684768 c propagations : 2841468 c inspects : 362417 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 212 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 184.21 c starts : 213 c conflicts : 0 c decisions : 2697432 c propagations : 2854871 c inspects : 364011 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 213 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 184.953 c starts : 214 c conflicts : 0 c decisions : 2710096 c propagations : 2868274 c inspects : 365641 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 214 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 186.043 c starts : 215 c conflicts : 0 c decisions : 2722760 c propagations : 2881677 c inspects : 367271 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 215 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 186.783 c starts : 216 c conflicts : 0 c decisions : 2735424 c propagations : 2895080 c inspects : 368901 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 216 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 187.526 c starts : 217 c conflicts : 0 c decisions : 2748088 c propagations : 2908483 c inspects : 370531 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 217 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 188.268 c starts : 218 c conflicts : 0 c decisions : 2760752 c propagations : 2921886 c inspects : 372161 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 218 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 189.013 c starts : 219 c conflicts : 0 c decisions : 2773416 c propagations : 2935289 c inspects : 373791 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 219 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 189.761 c starts : 220 c conflicts : 0 c decisions : 2786080 c propagations : 2948692 c inspects : 375421 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 220 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 190.832 c starts : 221 c conflicts : 0 c decisions : 2798744 c propagations : 2962095 c inspects : 377051 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 221 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 191.588 c starts : 222 c conflicts : 0 c decisions : 2811408 c propagations : 2975498 c inspects : 378681 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 222 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 192.342 c starts : 223 c conflicts : 0 c decisions : 2824072 c propagations : 2988901 c inspects : 380311 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 223 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 193.103 c starts : 224 c conflicts : 0 c decisions : 2836736 c propagations : 3002304 c inspects : 381941 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 224 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 193.841 c starts : 225 c conflicts : 0 c decisions : 2849400 c propagations : 3015707 c inspects : 383539 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 225 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 194.612 c starts : 226 c conflicts : 0 c decisions : 2862064 c propagations : 3029110 c inspects : 385169 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 226 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 195.721 c starts : 227 c conflicts : 0 c decisions : 2874728 c propagations : 3042513 c inspects : 386799 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 227 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 196.486 c starts : 228 c conflicts : 0 c decisions : 2887392 c propagations : 3055916 c inspects : 388429 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 228 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 197.234 c starts : 229 c conflicts : 0 c decisions : 2900056 c propagations : 3069319 c inspects : 390026 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 229 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 198.009 c starts : 230 c conflicts : 0 c decisions : 2912720 c propagations : 3082722 c inspects : 391656 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 230 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 198.785 c starts : 231 c conflicts : 0 c decisions : 2925384 c propagations : 3096125 c inspects : 393286 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 231 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 199.907 c starts : 232 c conflicts : 0 c decisions : 2938048 c propagations : 3109528 c inspects : 394916 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 232 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 200.659 c starts : 233 c conflicts : 0 c decisions : 2950712 c propagations : 3122931 c inspects : 396520 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 233 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 201.41 c starts : 234 c conflicts : 0 c decisions : 2963376 c propagations : 3136334 c inspects : 398113 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 234 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 202.187 c starts : 235 c conflicts : 0 c decisions : 2976040 c propagations : 3149737 c inspects : 399743 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 235 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 202.968 c starts : 236 c conflicts : 0 c decisions : 2988704 c propagations : 3163140 c inspects : 401373 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 236 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 203.759 c starts : 237 c conflicts : 0 c decisions : 3001368 c propagations : 3176543 c inspects : 403003 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 237 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 204.876 c starts : 238 c conflicts : 0 c decisions : 3014032 c propagations : 3189946 c inspects : 404633 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 238 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 205.641 c starts : 239 c conflicts : 0 c decisions : 3026696 c propagations : 3203349 c inspects : 406239 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 239 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 206.431 c starts : 240 c conflicts : 0 c decisions : 3039360 c propagations : 3216752 c inspects : 407869 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 240 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 207.222 c starts : 241 c conflicts : 0 c decisions : 3052024 c propagations : 3230155 c inspects : 409499 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 241 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 208.016 c starts : 242 c conflicts : 0 c decisions : 3064688 c propagations : 3243558 c inspects : 411129 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 242 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 208.814 c starts : 243 c conflicts : 0 c decisions : 3077352 c propagations : 3256961 c inspects : 412759 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 243 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 209.971 c starts : 244 c conflicts : 0 c decisions : 3090016 c propagations : 3270364 c inspects : 414389 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 244 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 210.77 c starts : 245 c conflicts : 0 c decisions : 3102680 c propagations : 3283767 c inspects : 416019 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 245 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 211.574 c starts : 246 c conflicts : 0 c decisions : 3115344 c propagations : 3297170 c inspects : 417649 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 246 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 212.354 c starts : 247 c conflicts : 0 c decisions : 3128008 c propagations : 3310573 c inspects : 419253 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 247 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 213.159 c starts : 248 c conflicts : 0 c decisions : 3140672 c propagations : 3323976 c inspects : 420883 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 248 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 214.313 c starts : 249 c conflicts : 0 c decisions : 3153336 c propagations : 3337379 c inspects : 422513 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 249 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 215.13 c starts : 250 c conflicts : 0 c decisions : 3166000 c propagations : 3350782 c inspects : 424143 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 250 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 215.944 c starts : 251 c conflicts : 0 c decisions : 3178664 c propagations : 3364185 c inspects : 425773 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 251 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 216.758 c starts : 252 c conflicts : 0 c decisions : 3191328 c propagations : 3377588 c inspects : 427403 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 252 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 217.576 c starts : 253 c conflicts : 0 c decisions : 3203992 c propagations : 3390991 c inspects : 429033 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 253 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 218.396 c starts : 254 c conflicts : 0 c decisions : 3216656 c propagations : 3404394 c inspects : 430663 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 254 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 219.517 c starts : 255 c conflicts : 0 c decisions : 3229320 c propagations : 3417797 c inspects : 432270 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 255 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 220.34 c starts : 256 c conflicts : 0 c decisions : 3241984 c propagations : 3431200 c inspects : 433900 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 256 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 221.383 c starts : 257 c conflicts : 0 c decisions : 3254648 c propagations : 3444603 c inspects : 435530 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 257 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 222.708 c starts : 258 c conflicts : 0 c decisions : 3267312 c propagations : 3458006 c inspects : 437133 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 258 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 223.538 c starts : 259 c conflicts : 0 c decisions : 3279976 c propagations : 3471409 c inspects : 438763 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 259 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 224.37 c starts : 260 c conflicts : 0 c decisions : 3292640 c propagations : 3484812 c inspects : 440393 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 260 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 225.204 c starts : 261 c conflicts : 0 c decisions : 3305304 c propagations : 3498215 c inspects : 442023 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 261 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 226.042 c starts : 262 c conflicts : 0 c decisions : 3317968 c propagations : 3511618 c inspects : 443653 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 262 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 227.139 c starts : 263 c conflicts : 0 c decisions : 3330632 c propagations : 3525021 c inspects : 445283 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 263 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 227.982 c starts : 264 c conflicts : 0 c decisions : 3343296 c propagations : 3538424 c inspects : 446913 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 264 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 228.826 c starts : 265 c conflicts : 0 c decisions : 3355960 c propagations : 3551827 c inspects : 448543 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 265 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 229.673 c starts : 266 c conflicts : 0 c decisions : 3368624 c propagations : 3565230 c inspects : 450173 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 266 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 230.5 c starts : 267 c conflicts : 0 c decisions : 3381288 c propagations : 3578633 c inspects : 451775 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 267 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 231.356 c starts : 268 c conflicts : 0 c decisions : 3393952 c propagations : 3592036 c inspects : 453405 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 268 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 232.589 c starts : 269 c conflicts : 0 c decisions : 3406616 c propagations : 3605439 c inspects : 455035 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 269 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 233.447 c starts : 270 c conflicts : 0 c decisions : 3419280 c propagations : 3618842 c inspects : 456665 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 270 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 234.303 c starts : 271 c conflicts : 0 c decisions : 3431944 c propagations : 3632245 c inspects : 458295 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 271 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 235.138 c starts : 272 c conflicts : 0 c decisions : 3444608 c propagations : 3645648 c inspects : 459897 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 272 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 235.976 c starts : 273 c conflicts : 0 c decisions : 3457272 c propagations : 3659051 c inspects : 461501 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 273 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 236.811 c starts : 274 c conflicts : 0 c decisions : 3469936 c propagations : 3672454 c inspects : 463091 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 274 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 238.014 c starts : 275 c conflicts : 0 c decisions : 3482600 c propagations : 3685857 c inspects : 464721 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 275 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 238.881 c starts : 276 c conflicts : 0 c decisions : 3495264 c propagations : 3699260 c inspects : 466351 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 276 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 239.75 c starts : 277 c conflicts : 0 c decisions : 3507928 c propagations : 3712663 c inspects : 467981 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 277 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 240.627 c starts : 278 c conflicts : 0 c decisions : 3520592 c propagations : 3726066 c inspects : 469611 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 278 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 241.499 c starts : 279 c conflicts : 0 c decisions : 3533256 c propagations : 3739469 c inspects : 471241 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 279 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 242.728 c starts : 280 c conflicts : 0 c decisions : 3545920 c propagations : 3752872 c inspects : 472871 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 280 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 243.606 c starts : 281 c conflicts : 0 c decisions : 3558584 c propagations : 3766275 c inspects : 474501 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 281 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 244.471 c starts : 282 c conflicts : 0 c decisions : 3571248 c propagations : 3779678 c inspects : 476089 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 282 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 245.359 c starts : 283 c conflicts : 0 c decisions : 3583912 c propagations : 3793081 c inspects : 477719 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 283 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 246.249 c starts : 284 c conflicts : 0 c decisions : 3596576 c propagations : 3806484 c inspects : 479349 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 284 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 247.143 c starts : 285 c conflicts : 0 c decisions : 3609240 c propagations : 3819887 c inspects : 480979 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 285 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 248.372 c starts : 286 c conflicts : 0 c decisions : 3621904 c propagations : 3833290 c inspects : 482609 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 286 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 249.24 c starts : 287 c conflicts : 0 c decisions : 3634568 c propagations : 3846693 c inspects : 484216 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 287 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 250.14 c starts : 288 c conflicts : 0 c decisions : 3647232 c propagations : 3860096 c inspects : 485846 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 288 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 251.04 c starts : 289 c conflicts : 0 c decisions : 3659896 c propagations : 3873499 c inspects : 487476 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 289 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 251.943 c starts : 290 c conflicts : 0 c decisions : 3672560 c propagations : 3886902 c inspects : 489106 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 290 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 252.849 c starts : 291 c conflicts : 0 c decisions : 3685224 c propagations : 3900305 c inspects : 490736 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 291 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 254.069 c starts : 292 c conflicts : 0 c decisions : 3697888 c propagations : 3913708 c inspects : 492338 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 292 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 254.947 c starts : 293 c conflicts : 0 c decisions : 3710552 c propagations : 3927111 c inspects : 493942 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 293 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 255.852 c starts : 294 c conflicts : 0 c decisions : 3723216 c propagations : 3940514 c inspects : 495572 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 294 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 256.757 c starts : 295 c conflicts : 0 c decisions : 3735880 c propagations : 3953917 c inspects : 497202 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 295 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 257.674 c starts : 296 c conflicts : 0 c decisions : 3748544 c propagations : 3967320 c inspects : 498832 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 296 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 258.909 c starts : 297 c conflicts : 0 c decisions : 3761208 c propagations : 3980723 c inspects : 500435 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 297 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 259.823 c starts : 298 c conflicts : 0 c decisions : 3773872 c propagations : 3994126 c inspects : 502065 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 298 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 260.739 c starts : 299 c conflicts : 0 c decisions : 3786536 c propagations : 4007529 c inspects : 503695 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 299 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 261.655 c starts : 300 c conflicts : 0 c decisions : 3799200 c propagations : 4020932 c inspects : 505325 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 300 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 262.574 c starts : 301 c conflicts : 0 c decisions : 3811864 c propagations : 4034335 c inspects : 506955 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 301 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 263.503 c starts : 302 c conflicts : 0 c decisions : 3824528 c propagations : 4047738 c inspects : 508585 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 302 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 264.735 c starts : 303 c conflicts : 0 c decisions : 3837192 c propagations : 4061141 c inspects : 510181 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 303 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 265.638 c starts : 304 c conflicts : 0 c decisions : 3849856 c propagations : 4074544 c inspects : 511785 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 304 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 266.542 c starts : 305 c conflicts : 0 c decisions : 3862520 c propagations : 4087947 c inspects : 513387 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 305 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 267.472 c starts : 306 c conflicts : 0 c decisions : 3875184 c propagations : 4101350 c inspects : 515017 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 306 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 268.404 c starts : 307 c conflicts : 0 c decisions : 3887848 c propagations : 4114753 c inspects : 516647 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 307 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 269.337 c starts : 308 c conflicts : 0 c decisions : 3900512 c propagations : 4128156 c inspects : 518277 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 308 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 270.627 c starts : 309 c conflicts : 0 c decisions : 3913176 c propagations : 4141559 c inspects : 519907 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 309 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 271.541 c starts : 310 c conflicts : 0 c decisions : 3925840 c propagations : 4154962 c inspects : 521511 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 310 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 272.456 c starts : 311 c conflicts : 0 c decisions : 3938504 c propagations : 4168365 c inspects : 523115 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 311 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 273.401 c starts : 312 c conflicts : 0 c decisions : 3951168 c propagations : 4181768 c inspects : 524745 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 312 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 274.32 c starts : 313 c conflicts : 0 c decisions : 3963832 c propagations : 4195171 c inspects : 526349 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 313 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 275.267 c starts : 314 c conflicts : 0 c decisions : 3976496 c propagations : 4208574 c inspects : 527979 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 314 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 276.569 c starts : 315 c conflicts : 0 c decisions : 3989160 c propagations : 4221977 c inspects : 529609 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 315 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 277.52 c starts : 316 c conflicts : 0 c decisions : 4001824 c propagations : 4235380 c inspects : 531239 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 316 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 278.473 c starts : 317 c conflicts : 0 c decisions : 4014488 c propagations : 4248783 c inspects : 532869 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 317 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 279.431 c starts : 318 c conflicts : 0 c decisions : 4027152 c propagations : 4262186 c inspects : 534499 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 318 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 280.398 c starts : 319 c conflicts : 0 c decisions : 4039816 c propagations : 4275589 c inspects : 536129 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 319 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 281.696 c starts : 320 c conflicts : 0 c decisions : 4052480 c propagations : 4288992 c inspects : 537759 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 320 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 282.658 c starts : 321 c conflicts : 0 c decisions : 4065144 c propagations : 4302395 c inspects : 539389 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 321 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 283.621 c starts : 322 c conflicts : 0 c decisions : 4077808 c propagations : 4315798 c inspects : 541019 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 322 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 284.589 c starts : 323 c conflicts : 0 c decisions : 4090472 c propagations : 4329201 c inspects : 542649 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 323 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 285.536 c starts : 324 c conflicts : 0 c decisions : 4103136 c propagations : 4342604 c inspects : 544256 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 324 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 286.481 c starts : 325 c conflicts : 0 c decisions : 4115800 c propagations : 4356007 c inspects : 545852 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 325 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 287.782 c starts : 326 c conflicts : 0 c decisions : 4128464 c propagations : 4369410 c inspects : 547482 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 326 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 288.755 c starts : 327 c conflicts : 0 c decisions : 4141128 c propagations : 4382813 c inspects : 549112 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 327 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 289.733 c starts : 328 c conflicts : 0 c decisions : 4153792 c propagations : 4396216 c inspects : 550742 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 328 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 290.715 c starts : 329 c conflicts : 0 c decisions : 4166456 c propagations : 4409619 c inspects : 552372 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 329 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 291.671 c starts : 330 c conflicts : 0 c decisions : 4179120 c propagations : 4423022 c inspects : 553974 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 330 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 293.007 c starts : 331 c conflicts : 0 c decisions : 4191784 c propagations : 4436425 c inspects : 555604 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 331 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 294.004 c starts : 332 c conflicts : 0 c decisions : 4204448 c propagations : 4449828 c inspects : 557234 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 332 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 295.001 c starts : 333 c conflicts : 0 c decisions : 4217112 c propagations : 4463231 c inspects : 558864 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 333 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 295.973 c starts : 334 c conflicts : 0 c decisions : 4229776 c propagations : 4476634 c inspects : 560466 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 334 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 296.973 c starts : 335 c conflicts : 0 c decisions : 4242440 c propagations : 4490037 c inspects : 562096 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 335 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 297.974 c starts : 336 c conflicts : 0 c decisions : 4255104 c propagations : 4503440 c inspects : 563726 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 336 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 299.312 c starts : 337 c conflicts : 0 c decisions : 4267768 c propagations : 4516843 c inspects : 565356 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 337 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 300.318 c starts : 338 c conflicts : 0 c decisions : 4280432 c propagations : 4530246 c inspects : 566986 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 338 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 301.328 c starts : 339 c conflicts : 0 c decisions : 4293096 c propagations : 4543649 c inspects : 568616 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 339 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 302.337 c starts : 340 c conflicts : 0 c decisions : 4305760 c propagations : 4557052 c inspects : 570246 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 340 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 303.349 c starts : 341 c conflicts : 0 c decisions : 4318424 c propagations : 4570455 c inspects : 571876 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 341 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 304.687 c starts : 342 c conflicts : 0 c decisions : 4331088 c propagations : 4583858 c inspects : 573506 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 342 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 305.702 c starts : 343 c conflicts : 0 c decisions : 4343752 c propagations : 4597261 c inspects : 575136 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 343 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 306.719 c starts : 344 c conflicts : 0 c decisions : 4356416 c propagations : 4610664 c inspects : 576766 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 344 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 307.744 c starts : 345 c conflicts : 0 c decisions : 4369080 c propagations : 4624067 c inspects : 578396 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 345 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 308.767 c starts : 346 c conflicts : 0 c decisions : 4381744 c propagations : 4637470 c inspects : 580026 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 346 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 309.792 c starts : 347 c conflicts : 0 c decisions : 4394408 c propagations : 4650873 c inspects : 581656 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 347 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 311.146 c starts : 348 c conflicts : 0 c decisions : 4407072 c propagations : 4664276 c inspects : 583286 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 348 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 312.143 c starts : 349 c conflicts : 0 c decisions : 4419736 c propagations : 4677679 c inspects : 584890 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 349 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 313.167 c starts : 350 c conflicts : 0 c decisions : 4432400 c propagations : 4691082 c inspects : 586520 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 350 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 314.207 c starts : 351 c conflicts : 0 c decisions : 4445064 c propagations : 4704485 c inspects : 588150 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 351 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 315.234 c starts : 352 c conflicts : 0 c decisions : 4457728 c propagations : 4717888 c inspects : 589780 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 352 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 316.589 c starts : 353 c conflicts : 0 c decisions : 4470392 c propagations : 4731291 c inspects : 591410 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 353 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 317.622 c starts : 354 c conflicts : 0 c decisions : 4483056 c propagations : 4744694 c inspects : 593040 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 354 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 318.657 c starts : 355 c conflicts : 0 c decisions : 4495720 c propagations : 4758097 c inspects : 594670 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 355 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 319.697 c starts : 356 c conflicts : 0 c decisions : 4508384 c propagations : 4771500 c inspects : 596300 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 356 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 320.715 c starts : 357 c conflicts : 0 c decisions : 4521048 c propagations : 4784903 c inspects : 597899 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 357 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 321.732 c starts : 358 c conflicts : 0 c decisions : 4533712 c propagations : 4798306 c inspects : 599502 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 358 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 323.107 c starts : 359 c conflicts : 0 c decisions : 4546376 c propagations : 4811709 c inspects : 601132 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 359 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 324.129 c starts : 360 c conflicts : 0 c decisions : 4559040 c propagations : 4825112 c inspects : 602734 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 360 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 325.176 c starts : 361 c conflicts : 0 c decisions : 4571704 c propagations : 4838515 c inspects : 604364 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 361 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 326.226 c starts : 362 c conflicts : 0 c decisions : 4584368 c propagations : 4851918 c inspects : 605994 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 362 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 327.276 c starts : 363 c conflicts : 0 c decisions : 4597032 c propagations : 4865321 c inspects : 607624 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 363 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 328.678 c starts : 364 c conflicts : 0 c decisions : 4609696 c propagations : 4878724 c inspects : 609254 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 364 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 329.711 c starts : 365 c conflicts : 0 c decisions : 4622360 c propagations : 4892127 c inspects : 610858 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 365 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 330.77 c starts : 366 c conflicts : 0 c decisions : 4635024 c propagations : 4905530 c inspects : 612488 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 366 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 331.83 c starts : 367 c conflicts : 0 c decisions : 4647688 c propagations : 4918933 c inspects : 614118 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 367 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 332.891 c starts : 368 c conflicts : 0 c decisions : 4660352 c propagations : 4932336 c inspects : 615748 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 368 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 333.954 c starts : 369 c conflicts : 0 c decisions : 4673016 c propagations : 4945739 c inspects : 617378 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 369 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 335.347 c starts : 370 c conflicts : 0 c decisions : 4685680 c propagations : 4959142 c inspects : 619008 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 370 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 336.416 c starts : 371 c conflicts : 0 c decisions : 4698344 c propagations : 4972545 c inspects : 620638 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 371 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 337.486 c starts : 372 c conflicts : 0 c decisions : 4711008 c propagations : 4985948 c inspects : 622268 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 372 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 338.559 c starts : 373 c conflicts : 0 c decisions : 4723672 c propagations : 4999351 c inspects : 623898 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 373 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 339.611 c starts : 374 c conflicts : 0 c decisions : 4736336 c propagations : 5012754 c inspects : 625501 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 374 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 341.025 c starts : 375 c conflicts : 0 c decisions : 4749000 c propagations : 5026157 c inspects : 627131 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 375 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 342.106 c starts : 376 c conflicts : 0 c decisions : 4761664 c propagations : 5039560 c inspects : 628761 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 376 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 343.189 c starts : 377 c conflicts : 0 c decisions : 4774328 c propagations : 5052963 c inspects : 630391 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 377 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 344.246 c starts : 378 c conflicts : 0 c decisions : 4786992 c propagations : 5066366 c inspects : 631984 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 378 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 345.333 c starts : 379 c conflicts : 0 c decisions : 4799656 c propagations : 5079769 c inspects : 633614 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 379 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 346.428 c starts : 380 c conflicts : 0 c decisions : 4812320 c propagations : 5093172 c inspects : 635244 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 380 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 347.851 c starts : 381 c conflicts : 0 c decisions : 4824984 c propagations : 5106575 c inspects : 636874 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 381 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 348.946 c starts : 382 c conflicts : 0 c decisions : 4837648 c propagations : 5119978 c inspects : 638504 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 382 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 350.041 c starts : 383 c conflicts : 0 c decisions : 4850312 c propagations : 5133381 c inspects : 640134 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 383 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 351.138 c starts : 384 c conflicts : 0 c decisions : 4862976 c propagations : 5146784 c inspects : 641764 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 384 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 352.244 c starts : 385 c conflicts : 0 c decisions : 4875640 c propagations : 5160187 c inspects : 643394 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 385 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 353.723 c starts : 386 c conflicts : 0 c decisions : 4888304 c propagations : 5173590 c inspects : 645024 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 386 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 354.827 c starts : 387 c conflicts : 0 c decisions : 4900968 c propagations : 5186993 c inspects : 646654 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 387 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 355.933 c starts : 388 c conflicts : 0 c decisions : 4913632 c propagations : 5200396 c inspects : 648284 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 388 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 357.039 c starts : 389 c conflicts : 0 c decisions : 4926296 c propagations : 5213799 c inspects : 649914 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 389 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 358.165 c starts : 390 c conflicts : 0 c decisions : 4938960 c propagations : 5227202 c inspects : 651544 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 390 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 359.615 c starts : 391 c conflicts : 0 c decisions : 4951624 c propagations : 5240605 c inspects : 653140 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 391 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 360.704 c starts : 392 c conflicts : 0 c decisions : 4964288 c propagations : 5254008 c inspects : 654744 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 392 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 361.793 c starts : 393 c conflicts : 0 c decisions : 4976952 c propagations : 5267411 c inspects : 656332 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 393 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 362.883 c starts : 394 c conflicts : 0 c decisions : 4989616 c propagations : 5280814 c inspects : 657925 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 394 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 364.006 c starts : 395 c conflicts : 0 c decisions : 5002280 c propagations : 5294217 c inspects : 659555 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 395 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 365.101 c starts : 396 c conflicts : 0 c decisions : 5014944 c propagations : 5307620 c inspects : 661151 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 396 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 366.573 c starts : 397 c conflicts : 0 c decisions : 5027608 c propagations : 5321023 c inspects : 662781 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 397 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 367.697 c starts : 398 c conflicts : 0 c decisions : 5040272 c propagations : 5334426 c inspects : 664411 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 398 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 368.823 c starts : 399 c conflicts : 0 c decisions : 5052936 c propagations : 5347829 c inspects : 666041 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 399 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 369.957 c starts : 400 c conflicts : 0 c decisions : 5065600 c propagations : 5361232 c inspects : 667671 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 400 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 371.088 c starts : 401 c conflicts : 0 c decisions : 5078264 c propagations : 5374635 c inspects : 669301 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 401 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 372.59 c starts : 402 c conflicts : 0 c decisions : 5090928 c propagations : 5388038 c inspects : 670931 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 402 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 373.726 c starts : 403 c conflicts : 0 c decisions : 5103592 c propagations : 5401441 c inspects : 672561 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 403 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 374.865 c starts : 404 c conflicts : 0 c decisions : 5116256 c propagations : 5414844 c inspects : 674191 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 404 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 376.006 c starts : 405 c conflicts : 0 c decisions : 5128920 c propagations : 5428247 c inspects : 675821 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 405 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 377.148 c starts : 406 c conflicts : 0 c decisions : 5141584 c propagations : 5441650 c inspects : 677451 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 406 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 378.297 c starts : 407 c conflicts : 0 c decisions : 5154248 c propagations : 5455053 c inspects : 679081 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 407 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 379.778 c starts : 408 c conflicts : 0 c decisions : 5166912 c propagations : 5468456 c inspects : 680711 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 408 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 380.927 c starts : 409 c conflicts : 0 c decisions : 5179576 c propagations : 5481859 c inspects : 682341 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 409 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 382.079 c starts : 410 c conflicts : 0 c decisions : 5192240 c propagations : 5495262 c inspects : 683971 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 410 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 383.207 c starts : 411 c conflicts : 0 c decisions : 5204904 c propagations : 5508665 c inspects : 685575 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 411 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 384.37 c starts : 412 c conflicts : 0 c decisions : 5217568 c propagations : 5522068 c inspects : 687205 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 412 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 385.867 c starts : 413 c conflicts : 0 c decisions : 5230232 c propagations : 5535471 c inspects : 688835 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 413 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 387.001 c starts : 414 c conflicts : 0 c decisions : 5242896 c propagations : 5548874 c inspects : 690440 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 414 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 388.165 c starts : 415 c conflicts : 0 c decisions : 5255560 c propagations : 5562277 c inspects : 692070 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 415 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 389.332 c starts : 416 c conflicts : 0 c decisions : 5268224 c propagations : 5575680 c inspects : 693700 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 416 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 390.507 c starts : 417 c conflicts : 0 c decisions : 5280888 c propagations : 5589083 c inspects : 695330 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 417 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 391.683 c starts : 418 c conflicts : 0 c decisions : 5293552 c propagations : 5602486 c inspects : 696960 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 418 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 393.187 c starts : 419 c conflicts : 0 c decisions : 5306216 c propagations : 5615889 c inspects : 698590 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 419 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 394.361 c starts : 420 c conflicts : 0 c decisions : 5318880 c propagations : 5629292 c inspects : 700220 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 420 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 395.511 c starts : 421 c conflicts : 0 c decisions : 5331544 c propagations : 5642695 c inspects : 701823 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 421 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 396.696 c starts : 422 c conflicts : 0 c decisions : 5344208 c propagations : 5656098 c inspects : 703453 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 422 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 397.859 c starts : 423 c conflicts : 0 c decisions : 5356872 c propagations : 5669501 c inspects : 705058 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 423 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 399.395 c starts : 424 c conflicts : 0 c decisions : 5369536 c propagations : 5682904 c inspects : 706688 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 424 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 400.578 c starts : 425 c conflicts : 0 c decisions : 5382200 c propagations : 5696307 c inspects : 708318 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 425 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 401.764 c starts : 426 c conflicts : 0 c decisions : 5394864 c propagations : 5709710 c inspects : 709948 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 426 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 402.954 c starts : 427 c conflicts : 0 c decisions : 5407528 c propagations : 5723113 c inspects : 711578 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 427 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 404.144 c starts : 428 c conflicts : 0 c decisions : 5420192 c propagations : 5736516 c inspects : 713208 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 428 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 405.313 c starts : 429 c conflicts : 0 c decisions : 5432856 c propagations : 5749919 c inspects : 714817 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 429 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 406.81 c starts : 430 c conflicts : 0 c decisions : 5445520 c propagations : 5763322 c inspects : 716421 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 430 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 408.007 c starts : 431 c conflicts : 0 c decisions : 5458184 c propagations : 5776725 c inspects : 718051 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 431 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 409.207 c starts : 432 c conflicts : 0 c decisions : 5470848 c propagations : 5790128 c inspects : 719681 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 432 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 410.382 c starts : 433 c conflicts : 0 c decisions : 5483512 c propagations : 5803531 c inspects : 721285 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 433 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 411.586 c starts : 434 c conflicts : 0 c decisions : 5496176 c propagations : 5816934 c inspects : 722915 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 434 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 413.113 c starts : 435 c conflicts : 0 c decisions : 5508840 c propagations : 5830337 c inspects : 724519 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 435 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 414.319 c starts : 436 c conflicts : 0 c decisions : 5521504 c propagations : 5843740 c inspects : 726149 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 436 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 415.526 c starts : 437 c conflicts : 0 c decisions : 5534168 c propagations : 5857143 c inspects : 727779 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 437 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 416.735 c starts : 438 c conflicts : 0 c decisions : 5546832 c propagations : 5870546 c inspects : 729409 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 438 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 417.947 c starts : 439 c conflicts : 0 c decisions : 5559496 c propagations : 5883949 c inspects : 731039 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 439 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 419.163 c starts : 440 c conflicts : 0 c decisions : 5572160 c propagations : 5897352 c inspects : 732669 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 440 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 420.716 c starts : 441 c conflicts : 0 c decisions : 5584824 c propagations : 5910755 c inspects : 734299 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 441 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 421.934 c starts : 442 c conflicts : 0 c decisions : 5597488 c propagations : 5924158 c inspects : 735929 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 442 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 423.155 c starts : 443 c conflicts : 0 c decisions : 5610152 c propagations : 5937561 c inspects : 737559 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 443 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 424.353 c starts : 444 c conflicts : 0 c decisions : 5622816 c propagations : 5950964 c inspects : 739161 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 444 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 425.581 c starts : 445 c conflicts : 0 c decisions : 5635480 c propagations : 5964367 c inspects : 740791 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 445 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 427.136 c starts : 446 c conflicts : 0 c decisions : 5648144 c propagations : 5977770 c inspects : 742393 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 446 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 428.365 c starts : 447 c conflicts : 0 c decisions : 5660808 c propagations : 5991173 c inspects : 744023 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 447 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 429.572 c starts : 448 c conflicts : 0 c decisions : 5673472 c propagations : 6004576 c inspects : 745609 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 448 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 430.804 c starts : 449 c conflicts : 0 c decisions : 5686136 c propagations : 6017979 c inspects : 747239 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 449 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 432.039 c starts : 450 c conflicts : 0 c decisions : 5698800 c propagations : 6031382 c inspects : 748869 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 450 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 433.278 c starts : 451 c conflicts : 0 c decisions : 5711464 c propagations : 6044785 c inspects : 750499 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 451 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 434.847 c starts : 452 c conflicts : 0 c decisions : 5724128 c propagations : 6058188 c inspects : 752129 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 452 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 436.091 c starts : 453 c conflicts : 0 c decisions : 5736792 c propagations : 6071591 c inspects : 753759 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 453 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 437.31 c starts : 454 c conflicts : 0 c decisions : 5749456 c propagations : 6084994 c inspects : 755363 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 454 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 438.558 c starts : 455 c conflicts : 0 c decisions : 5762120 c propagations : 6098397 c inspects : 756993 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 455 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 439.807 c starts : 456 c conflicts : 0 c decisions : 5774784 c propagations : 6111800 c inspects : 758623 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 456 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 441.387 c starts : 457 c conflicts : 0 c decisions : 5787448 c propagations : 6125203 c inspects : 760253 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 457 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 442.639 c starts : 458 c conflicts : 0 c decisions : 5800112 c propagations : 6138606 c inspects : 761883 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 458 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 443.893 c starts : 459 c conflicts : 0 c decisions : 5812776 c propagations : 6152009 c inspects : 763513 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 459 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 445.152 c starts : 460 c conflicts : 0 c decisions : 5825440 c propagations : 6165412 c inspects : 765143 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 460 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 446.419 c starts : 461 c conflicts : 0 c decisions : 5838104 c propagations : 6178815 c inspects : 766773 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 461 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 448.019 c starts : 462 c conflicts : 0 c decisions : 5850768 c propagations : 6192218 c inspects : 768403 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 462 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 449.283 c starts : 463 c conflicts : 0 c decisions : 5863432 c propagations : 6205621 c inspects : 770033 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 463 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 450.552 c starts : 464 c conflicts : 0 c decisions : 5876096 c propagations : 6219024 c inspects : 771663 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 464 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 451.8 c starts : 465 c conflicts : 0 c decisions : 5888760 c propagations : 6232427 c inspects : 773267 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 465 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 453.081 c starts : 466 c conflicts : 0 c decisions : 5901424 c propagations : 6245830 c inspects : 774897 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 466 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 454.362 c starts : 467 c conflicts : 0 c decisions : 5914088 c propagations : 6259233 c inspects : 776527 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 467 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 455.974 c starts : 468 c conflicts : 0 c decisions : 5926752 c propagations : 6272636 c inspects : 778157 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 468 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 457.25 c starts : 469 c conflicts : 0 c decisions : 5939416 c propagations : 6286039 c inspects : 779787 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 469 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 458.53 c starts : 470 c conflicts : 0 c decisions : 5952080 c propagations : 6299442 c inspects : 781417 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 470 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 459.79 c starts : 471 c conflicts : 0 c decisions : 5964744 c propagations : 6312845 c inspects : 783021 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 471 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 461.049 c starts : 472 c conflicts : 0 c decisions : 5977408 c propagations : 6326248 c inspects : 784623 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 472 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 462.658 c starts : 473 c conflicts : 0 c decisions : 5990072 c propagations : 6339651 c inspects : 786216 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 473 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 463.923 c starts : 474 c conflicts : 0 c decisions : 6002736 c propagations : 6353054 c inspects : 787820 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 474 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 465.21 c starts : 475 c conflicts : 0 c decisions : 6015400 c propagations : 6366457 c inspects : 789450 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 475 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 466.502 c starts : 476 c conflicts : 0 c decisions : 6028064 c propagations : 6379860 c inspects : 791080 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 476 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 467.795 c starts : 477 c conflicts : 0 c decisions : 6040728 c propagations : 6393263 c inspects : 792710 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 477 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 469.088 c starts : 478 c conflicts : 0 c decisions : 6053392 c propagations : 6406666 c inspects : 794340 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 478 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 470.726 c starts : 479 c conflicts : 0 c decisions : 6066056 c propagations : 6420069 c inspects : 795970 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 479 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 472.002 c starts : 480 c conflicts : 0 c decisions : 6078720 c propagations : 6433472 c inspects : 797574 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 480 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 473.303 c starts : 481 c conflicts : 0 c decisions : 6091384 c propagations : 6446875 c inspects : 799204 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 481 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 474.607 c starts : 482 c conflicts : 0 c decisions : 6104048 c propagations : 6460278 c inspects : 800834 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 482 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 475.913 c starts : 483 c conflicts : 0 c decisions : 6116712 c propagations : 6473681 c inspects : 802464 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 483 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 477.577 c starts : 484 c conflicts : 0 c decisions : 6129376 c propagations : 6487084 c inspects : 804094 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 484 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 478.888 c starts : 485 c conflicts : 0 c decisions : 6142040 c propagations : 6500487 c inspects : 805724 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 485 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 480.202 c starts : 486 c conflicts : 0 c decisions : 6154704 c propagations : 6513890 c inspects : 807354 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 486 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 481.519 c starts : 487 c conflicts : 0 c decisions : 6167368 c propagations : 6527293 c inspects : 808984 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 487 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 482.835 c starts : 488 c conflicts : 0 c decisions : 6180032 c propagations : 6540696 c inspects : 810614 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 488 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 484.153 c starts : 489 c conflicts : 0 c decisions : 6192696 c propagations : 6554099 c inspects : 812244 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 489 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 485.806 c starts : 490 c conflicts : 0 c decisions : 6205360 c propagations : 6567502 c inspects : 813874 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 490 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 487.129 c starts : 491 c conflicts : 0 c decisions : 6218024 c propagations : 6580905 c inspects : 815504 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 491 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 488.454 c starts : 492 c conflicts : 0 c decisions : 6230688 c propagations : 6594308 c inspects : 817134 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 492 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 489.782 c starts : 493 c conflicts : 0 c decisions : 6243352 c propagations : 6607711 c inspects : 818764 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 493 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 491.111 c starts : 494 c conflicts : 0 c decisions : 6256016 c propagations : 6621114 c inspects : 820394 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 494 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 492.767 c starts : 495 c conflicts : 0 c decisions : 6268680 c propagations : 6634517 c inspects : 822024 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 495 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 494.1 c starts : 496 c conflicts : 0 c decisions : 6281344 c propagations : 6647920 c inspects : 823654 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 496 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 495.436 c starts : 497 c conflicts : 0 c decisions : 6294008 c propagations : 6661323 c inspects : 825284 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 497 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 496.775 c starts : 498 c conflicts : 0 c decisions : 6306672 c propagations : 6674726 c inspects : 826914 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 498 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 498.115 c starts : 499 c conflicts : 0 c decisions : 6319336 c propagations : 6688129 c inspects : 828544 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 499 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 499.762 c starts : 500 c conflicts : 0 c decisions : 6332000 c propagations : 6701532 c inspects : 830174 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 500 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 501.108 c starts : 501 c conflicts : 0 c decisions : 6344664 c propagations : 6714935 c inspects : 831804 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 501 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 502.454 c starts : 502 c conflicts : 0 c decisions : 6357328 c propagations : 6728338 c inspects : 833434 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 502 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 503.776 c starts : 503 c conflicts : 0 c decisions : 6369992 c propagations : 6741741 c inspects : 835021 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 503 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 505.127 c starts : 504 c conflicts : 0 c decisions : 6382656 c propagations : 6755144 c inspects : 836651 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 504 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 506.455 c starts : 505 c conflicts : 0 c decisions : 6395320 c propagations : 6768547 c inspects : 838253 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 505 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 508.15 c starts : 506 c conflicts : 0 c decisions : 6407984 c propagations : 6781950 c inspects : 839883 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 506 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 509.518 c starts : 507 c conflicts : 0 c decisions : 6420648 c propagations : 6795353 c inspects : 841513 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 507 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 510.89 c starts : 508 c conflicts : 0 c decisions : 6433312 c propagations : 6808756 c inspects : 843143 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 508 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 512.239 c starts : 509 c conflicts : 0 c decisions : 6445976 c propagations : 6822159 c inspects : 844740 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 509 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 513.589 c starts : 510 c conflicts : 0 c decisions : 6458640 c propagations : 6835562 c inspects : 846346 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 510 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 515.296 c starts : 511 c conflicts : 0 c decisions : 6471304 c propagations : 6848965 c inspects : 847976 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 511 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 516.665 c starts : 512 c conflicts : 0 c decisions : 6483968 c propagations : 6862368 c inspects : 849606 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 512 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 518.036 c starts : 513 c conflicts : 0 c decisions : 6496632 c propagations : 6875771 c inspects : 851236 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 513 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 537.063 c starts : 514 c conflicts : 0 c decisions : 6509296 c propagations : 6889174 c inspects : 852866 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 514 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 538.438 c starts : 515 c conflicts : 0 c decisions : 6521960 c propagations : 6902577 c inspects : 854496 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 515 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 539.799 c starts : 516 c conflicts : 0 c decisions : 6534624 c propagations : 6915980 c inspects : 856100 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 516 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 541.188 c starts : 517 c conflicts : 0 c decisions : 6547288 c propagations : 6929383 c inspects : 857730 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 517 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 542.579 c starts : 518 c conflicts : 0 c decisions : 6559952 c propagations : 6942786 c inspects : 859360 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 518 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 557.039 c starts : 519 c conflicts : 0 c decisions : 6572616 c propagations : 6956189 c inspects : 860990 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 519 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 558.437 c starts : 520 c conflicts : 0 c decisions : 6585280 c propagations : 6969592 c inspects : 862620 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 520 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 559.811 c starts : 521 c conflicts : 0 c decisions : 6597944 c propagations : 6982995 c inspects : 864221 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 521 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 561.187 c starts : 522 c conflicts : 0 c decisions : 6610608 c propagations : 6996398 c inspects : 865826 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 522 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 562.589 c starts : 523 c conflicts : 0 c decisions : 6623272 c propagations : 7009801 c inspects : 867456 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 523 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 563.993 c starts : 524 c conflicts : 0 c decisions : 6635936 c propagations : 7023204 c inspects : 869086 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 524 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 578.571 c starts : 525 c conflicts : 0 c decisions : 6648600 c propagations : 7036607 c inspects : 870716 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 525 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 579.97 c starts : 526 c conflicts : 0 c decisions : 6661264 c propagations : 7050010 c inspects : 872346 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 526 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 581.376 c starts : 527 c conflicts : 0 c decisions : 6673928 c propagations : 7063413 c inspects : 873976 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 527 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 582.777 c starts : 528 c conflicts : 0 c decisions : 6686592 c propagations : 7076816 c inspects : 875606 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 528 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 584.163 c starts : 529 c conflicts : 0 c decisions : 6699256 c propagations : 7090219 c inspects : 877210 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 529 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 605.003 c starts : 530 c conflicts : 0 c decisions : 6711920 c propagations : 7103622 c inspects : 878840 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 530 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 606.401 c starts : 531 c conflicts : 0 c decisions : 6724584 c propagations : 7117025 c inspects : 880425 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 531 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 607.795 c starts : 532 c conflicts : 0 c decisions : 6737248 c propagations : 7130428 c inspects : 882027 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 532 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 609.218 c starts : 533 c conflicts : 0 c decisions : 6749912 c propagations : 7143831 c inspects : 883657 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 533 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 610.645 c starts : 534 c conflicts : 0 c decisions : 6762576 c propagations : 7157234 c inspects : 885287 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 534 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 612.047 c starts : 535 c conflicts : 0 c decisions : 6775240 c propagations : 7170637 c inspects : 886893 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 535 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 626.914 c starts : 536 c conflicts : 0 c decisions : 6787904 c propagations : 7184040 c inspects : 888523 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 536 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 628.333 c starts : 537 c conflicts : 0 c decisions : 6800568 c propagations : 7197443 c inspects : 890153 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 537 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 629.757 c starts : 538 c conflicts : 0 c decisions : 6813232 c propagations : 7210846 c inspects : 891783 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 538 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 631.182 c starts : 539 c conflicts : 0 c decisions : 6825896 c propagations : 7224249 c inspects : 893413 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 539 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 632.583 c starts : 540 c conflicts : 0 c decisions : 6838560 c propagations : 7237652 c inspects : 895017 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 540 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 647.608 c starts : 541 c conflicts : 0 c decisions : 6851224 c propagations : 7251055 c inspects : 896647 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 541 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 649.014 c starts : 542 c conflicts : 0 c decisions : 6863888 c propagations : 7264458 c inspects : 898253 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 542 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 650.453 c starts : 543 c conflicts : 0 c decisions : 6876552 c propagations : 7277861 c inspects : 899883 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 543 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 651.9 c starts : 544 c conflicts : 0 c decisions : 6889216 c propagations : 7291264 c inspects : 901513 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 544 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 653.347 c starts : 545 c conflicts : 0 c decisions : 6901880 c propagations : 7304667 c inspects : 903143 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 545 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 654.797 c starts : 546 c conflicts : 0 c decisions : 6914544 c propagations : 7318070 c inspects : 904773 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 546 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 669.975 c starts : 547 c conflicts : 0 c decisions : 6927208 c propagations : 7331473 c inspects : 906403 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 547 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 671.419 c starts : 548 c conflicts : 0 c decisions : 6939872 c propagations : 7344876 c inspects : 908033 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 548 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 672.882 c starts : 549 c conflicts : 0 c decisions : 6952536 c propagations : 7358279 c inspects : 909663 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 549 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 674.341 c starts : 550 c conflicts : 0 c decisions : 6965200 c propagations : 7371682 c inspects : 911293 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 550 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 675.803 c starts : 551 c conflicts : 0 c decisions : 6977864 c propagations : 7385085 c inspects : 912923 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 551 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 691.286 c starts : 552 c conflicts : 0 c decisions : 6990528 c propagations : 7398488 c inspects : 914553 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 552 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 692.713 c starts : 553 c conflicts : 0 c decisions : 7003192 c propagations : 7411891 c inspects : 916139 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 553 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 694.175 c starts : 554 c conflicts : 0 c decisions : 7015856 c propagations : 7425294 c inspects : 917769 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 554 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 695.633 c starts : 555 c conflicts : 0 c decisions : 7028520 c propagations : 7438697 c inspects : 919399 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 555 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 697.094 c starts : 556 c conflicts : 0 c decisions : 7041184 c propagations : 7452100 c inspects : 921029 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 556 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 712.509 c starts : 557 c conflicts : 0 c decisions : 7053848 c propagations : 7465503 c inspects : 922632 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 557 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 713.973 c starts : 558 c conflicts : 0 c decisions : 7066512 c propagations : 7478906 c inspects : 924262 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 558 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 715.439 c starts : 559 c conflicts : 0 c decisions : 7079176 c propagations : 7492309 c inspects : 925892 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 559 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 716.909 c starts : 560 c conflicts : 0 c decisions : 7091840 c propagations : 7505712 c inspects : 927522 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 560 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 718.363 c starts : 561 c conflicts : 0 c decisions : 7104504 c propagations : 7519115 c inspects : 929129 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 561 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 719.847 c starts : 562 c conflicts : 0 c decisions : 7117168 c propagations : 7532518 c inspects : 930759 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 562 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 735.422 c starts : 563 c conflicts : 0 c decisions : 7129832 c propagations : 7545921 c inspects : 932389 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 563 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 736.908 c starts : 564 c conflicts : 0 c decisions : 7142496 c propagations : 7559324 c inspects : 934019 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 564 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 738.373 c starts : 565 c conflicts : 0 c decisions : 7155160 c propagations : 7572727 c inspects : 935605 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 565 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 739.867 c starts : 566 c conflicts : 0 c decisions : 7167824 c propagations : 7586130 c inspects : 937235 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 566 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 741.338 c starts : 567 c conflicts : 0 c decisions : 7180488 c propagations : 7599533 c inspects : 938832 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 567 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 757.026 c starts : 568 c conflicts : 0 c decisions : 7193152 c propagations : 7612936 c inspects : 940462 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 568 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 758.515 c starts : 569 c conflicts : 0 c decisions : 7205816 c propagations : 7626339 c inspects : 942092 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 569 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 759.994 c starts : 570 c conflicts : 0 c decisions : 7218480 c propagations : 7639742 c inspects : 943697 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 570 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 761.467 c starts : 571 c conflicts : 0 c decisions : 7231144 c propagations : 7653145 c inspects : 945301 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 571 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 762.936 c starts : 572 c conflicts : 0 c decisions : 7243808 c propagations : 7666548 c inspects : 946903 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 572 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 764.434 c starts : 573 c conflicts : 0 c decisions : 7256472 c propagations : 7679951 c inspects : 948533 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 573 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 780.472 c starts : 574 c conflicts : 0 c decisions : 7269136 c propagations : 7693354 c inspects : 950163 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 574 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 781.951 c starts : 575 c conflicts : 0 c decisions : 7281800 c propagations : 7706757 c inspects : 951765 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 575 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 783.434 c starts : 576 c conflicts : 0 c decisions : 7294464 c propagations : 7720160 c inspects : 953359 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 576 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 784.938 c starts : 577 c conflicts : 0 c decisions : 7307128 c propagations : 7733563 c inspects : 954989 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 577 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 786.445 c starts : 578 c conflicts : 0 c decisions : 7319792 c propagations : 7746966 c inspects : 956619 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 578 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 802.407 c starts : 579 c conflicts : 0 c decisions : 7332456 c propagations : 7760369 c inspects : 958249 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 579 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 803.919 c starts : 580 c conflicts : 0 c decisions : 7345120 c propagations : 7773772 c inspects : 959879 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 580 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 805.41 c starts : 581 c conflicts : 0 c decisions : 7357784 c propagations : 7787175 c inspects : 961483 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 581 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 806.905 c starts : 582 c conflicts : 0 c decisions : 7370448 c propagations : 7800578 c inspects : 963086 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 582 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 808.42 c starts : 583 c conflicts : 0 c decisions : 7383112 c propagations : 7813981 c inspects : 964698 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 583 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 809.951 c starts : 584 c conflicts : 0 c decisions : 7395776 c propagations : 7827384 c inspects : 966328 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 584 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 826.055 c starts : 585 c conflicts : 0 c decisions : 7408440 c propagations : 7840787 c inspects : 967958 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 585 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 827.578 c starts : 586 c conflicts : 0 c decisions : 7421104 c propagations : 7854190 c inspects : 969588 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 586 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 829.106 c starts : 587 c conflicts : 0 c decisions : 7433768 c propagations : 7867593 c inspects : 971218 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 587 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 830.615 c starts : 588 c conflicts : 0 c decisions : 7446432 c propagations : 7880996 c inspects : 972823 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 588 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 832.132 c starts : 589 c conflicts : 0 c decisions : 7459096 c propagations : 7894399 c inspects : 974427 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 589 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 849.368 c starts : 590 c conflicts : 0 c decisions : 7471760 c propagations : 7907802 c inspects : 976057 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 590 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 850.904 c starts : 591 c conflicts : 0 c decisions : 7484424 c propagations : 7921205 c inspects : 977687 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 591 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 852.441 c starts : 592 c conflicts : 0 c decisions : 7497088 c propagations : 7934608 c inspects : 979317 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 592 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 853.977 c starts : 593 c conflicts : 0 c decisions : 7509752 c propagations : 7948011 c inspects : 980947 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 593 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 855.555 c starts : 594 c conflicts : 0 c decisions : 7522416 c propagations : 7961414 c inspects : 982577 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 594 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 878.549 c starts : 595 c conflicts : 0 c decisions : 7535080 c propagations : 7974817 c inspects : 984181 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 595 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 880.102 c starts : 596 c conflicts : 0 c decisions : 7547744 c propagations : 7988220 c inspects : 985811 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 596 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 881.651 c starts : 597 c conflicts : 0 c decisions : 7560408 c propagations : 8001623 c inspects : 987441 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 597 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 883.201 c starts : 598 c conflicts : 0 c decisions : 7573072 c propagations : 8015026 c inspects : 989071 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 598 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 885.139 c starts : 599 c conflicts : 0 c decisions : 7585736 c propagations : 8028429 c inspects : 990701 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 599 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 901.963 c starts : 600 c conflicts : 0 c decisions : 7598400 c propagations : 8041832 c inspects : 992331 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 600 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 903.527 c starts : 601 c conflicts : 0 c decisions : 7611064 c propagations : 8055235 c inspects : 993961 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 601 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 905.096 c starts : 602 c conflicts : 0 c decisions : 7623728 c propagations : 8068638 c inspects : 995591 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 602 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 906.853 c starts : 603 c conflicts : 0 c decisions : 7636392 c propagations : 8082041 c inspects : 997221 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 603 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 924.021 c starts : 604 c conflicts : 0 c decisions : 7649056 c propagations : 8095444 c inspects : 998851 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 604 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 925.56 c starts : 605 c conflicts : 0 c decisions : 7661720 c propagations : 8108847 c inspects : 1000438 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 605 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 927.115 c starts : 606 c conflicts : 0 c decisions : 7674384 c propagations : 8122250 c inspects : 1002042 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 606 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 928.765 c starts : 607 c conflicts : 0 c decisions : 7687048 c propagations : 8135653 c inspects : 1003672 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 607 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 946.2 c starts : 608 c conflicts : 0 c decisions : 7699712 c propagations : 8149056 c inspects : 1005302 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 608 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 947.773 c starts : 609 c conflicts : 0 c decisions : 7712376 c propagations : 8162459 c inspects : 1006932 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 609 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 949.323 c starts : 610 c conflicts : 0 c decisions : 7725040 c propagations : 8175862 c inspects : 1008529 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 610 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 951.261 c starts : 611 c conflicts : 0 c decisions : 7737704 c propagations : 8189265 c inspects : 1010159 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 611 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 974.303 c starts : 612 c conflicts : 0 c decisions : 7750368 c propagations : 8202668 c inspects : 1011789 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 612 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 975.868 c starts : 613 c conflicts : 0 c decisions : 7763032 c propagations : 8216071 c inspects : 1013382 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 613 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 977.461 c starts : 614 c conflicts : 0 c decisions : 7775696 c propagations : 8229474 c inspects : 1015012 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 614 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 995.012 c starts : 615 c conflicts : 0 c decisions : 7788360 c propagations : 8242877 c inspects : 1016616 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 615 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 996.6 c starts : 616 c conflicts : 0 c decisions : 7801024 c propagations : 8256280 c inspects : 1018246 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 616 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 998.191 c starts : 617 c conflicts : 0 c decisions : 7813688 c propagations : 8269683 c inspects : 1019876 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 617 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1015.752 c starts : 618 c conflicts : 0 c decisions : 7826352 c propagations : 8283086 c inspects : 1021480 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 618 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1017.351 c starts : 619 c conflicts : 0 c decisions : 7839016 c propagations : 8296489 c inspects : 1023110 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 619 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1019.074 c starts : 620 c conflicts : 0 c decisions : 7851680 c propagations : 8309892 c inspects : 1024740 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 620 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1036.68 c starts : 621 c conflicts : 0 c decisions : 7864344 c propagations : 8323295 c inspects : 1026370 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 621 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1038.281 c starts : 622 c conflicts : 0 c decisions : 7877008 c propagations : 8336698 c inspects : 1028000 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 622 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1040.494 c starts : 623 c conflicts : 0 c decisions : 7889672 c propagations : 8350101 c inspects : 1029630 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 623 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1057.463 c starts : 624 c conflicts : 0 c decisions : 7902336 c propagations : 8363504 c inspects : 1031224 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 624 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1059.051 c starts : 625 c conflicts : 0 c decisions : 7915000 c propagations : 8376907 c inspects : 1032815 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 625 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1076.829 c starts : 626 c conflicts : 0 c decisions : 7927664 c propagations : 8390310 c inspects : 1034445 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 626 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1078.452 c starts : 627 c conflicts : 0 c decisions : 7940328 c propagations : 8403713 c inspects : 1036075 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 627 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1096.258 c starts : 628 c conflicts : 0 c decisions : 7952992 c propagations : 8417116 c inspects : 1037705 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 628 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1097.873 c starts : 629 c conflicts : 0 c decisions : 7965656 c propagations : 8430519 c inspects : 1039335 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 629 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1115.715 c starts : 630 c conflicts : 0 c decisions : 7978320 c propagations : 8443922 c inspects : 1040965 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 630 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1117.36 c starts : 631 c conflicts : 0 c decisions : 7990984 c propagations : 8457325 c inspects : 1042558 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 631 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1140.949 c starts : 632 c conflicts : 0 c decisions : 8003648 c propagations : 8470728 c inspects : 1044188 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 632 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1142.951 c starts : 633 c conflicts : 0 c decisions : 8016312 c propagations : 8484131 c inspects : 1045818 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 633 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1160.368 c starts : 634 c conflicts : 0 c decisions : 8028976 c propagations : 8497534 c inspects : 1047448 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 634 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1178.264 c starts : 635 c conflicts : 0 c decisions : 8041640 c propagations : 8510937 c inspects : 1049078 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 635 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1180.251 c starts : 636 c conflicts : 0 c decisions : 8054304 c propagations : 8524340 c inspects : 1050683 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 636 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1197.645 c starts : 637 c conflicts : 0 c decisions : 8066968 c propagations : 8537743 c inspects : 1052272 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 637 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1215.626 c starts : 638 c conflicts : 0 c decisions : 8079632 c propagations : 8551146 c inspects : 1053902 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 638 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1233.582 c starts : 639 c conflicts : 0 c decisions : 8092296 c propagations : 8564549 c inspects : 1055532 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 639 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1251.567 c starts : 640 c conflicts : 0 c decisions : 8104960 c propagations : 8577952 c inspects : 1057162 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 640 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1269.5 c starts : 641 c conflicts : 0 c decisions : 8117624 c propagations : 8591355 c inspects : 1058755 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 641 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1287.605 c starts : 642 c conflicts : 0 c decisions : 8130288 c propagations : 8604758 c inspects : 1060385 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 642 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1305.878 c starts : 643 c conflicts : 0 c decisions : 8142952 c propagations : 8618161 c inspects : 1062015 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 643 c c CURRENT OPTIMUM=280363008 c Current CPU time (ms) : 1324.21 c starts : 644 c conflicts : 0 c decisions : 8155616 c propagations : 8631564 c inspects : 1063645 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 644 c c CURRENT OPTIMUM=280363008 Exception in thread "main" java.lang.OutOfMemoryError: Java heap space #### 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.79 0.95 0.93 2/54 15594 Raw data (stat): 15594 (runsolver) R 15593 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540003392 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.82 0.95 0.93 2/63 15603 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 17981 0 1 0 887 40 0 0 25 0 10 0 540003392 853499904 19115 4294967295 134512640 134569956 3221224400 3221214180 1077589904 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 208374 19115 13073 16 0 208358 0 vsize: 833496 [startup+20.0004 s] Raw data (loadavg): 0.85 0.95 0.93 2/63 15603 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 17981 0 1 0 1775 40 0 0 25 0 10 0 540003392 853774336 19708 4294967295 134512640 134569956 3221224400 3221214716 1079677938 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 208441 19708 13073 16 0 208425 0 vsize: 833764 [startup+30.0003 s] Raw data (loadavg): 0.87 0.95 0.93 2/63 15603 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 17981 0 1 0 2675 40 0 0 25 0 10 0 540003392 853774336 20148 4294967295 134512640 134569956 3221224400 3221214824 1131222723 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 208441 20148 13073 16 0 208425 0 vsize: 833764 [startup+40.0009 s] Raw data (loadavg): 0.89 0.95 0.93 2/63 15603 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 17981 0 1 0 3605 40 0 0 25 0 10 0 540003392 853774336 20378 4294967295 134512640 134569956 3221224400 3221214824 1131220421 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 208441 20378 13073 16 0 208425 0 vsize: 833764 [startup+50.0019 s] Raw data (loadavg): 0.91 0.96 0.93 2/63 15603 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 17981 0 1 0 4533 41 0 0 25 0 10 0 540003392 853774336 20501 4294967295 134512640 134569956 3221224400 3221214824 1131222189 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 208441 20501 13073 16 0 208425 0 vsize: 833764 [startup+60.0016 s] Raw data (loadavg): 1.00 0.97 0.93 2/63 15603 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 17985 0 1 0 5470 42 0 0 25 0 10 0 540003392 858271744 21575 4294967295 134512640 134569956 3221224400 3221214808 1131149183 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209539 21575 13073 16 0 209523 0 vsize: 838156 [startup+70.0027 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15620 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18016 3 1 0 6322 44 0 0 25 0 11 0 540003392 858800128 27384 4294967295 134512640 134569956 3221224400 3221214912 1131420804 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 27384 13073 16 0 209652 0 vsize: 838672 [startup+80.0031 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15645 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18016 3 1 0 7179 45 1 0 25 0 11 0 540003392 858800128 34042 4294967295 134512640 134569956 3221224400 3221214912 1131420640 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 34042 13073 16 0 209652 0 vsize: 838672 [startup+90.0028 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15667 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18016 3 1 0 8035 46 2 1 25 0 11 0 540003392 858800128 39632 4294967295 134512640 134569956 3221224400 3221214800 1131276287 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 39632 13073 16 0 209652 0 vsize: 838672 [startup+100.003 s] Raw data (loadavg): 1.00 0.97 0.93 2/63 15687 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18016 3 1 0 8930 47 2 1 25 0 10 0 540003392 858800128 45473 4294967295 134512640 134569956 3221224400 3221214656 1131258100 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 45473 13073 16 0 209652 0 vsize: 838672 [startup+110.004 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15706 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18016 3 1 0 9823 49 3 1 25 0 11 0 540003392 858800128 49520 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 49520 13073 16 0 209652 0 vsize: 838672 [startup+120.004 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15723 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18016 3 1 0 10704 50 3 1 25 0 11 0 540003392 858800128 53898 4294967295 134512640 134569956 3221224400 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 53898 13073 16 0 209652 0 vsize: 838672 [startup+130.005 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15739 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18016 3 1 0 11590 51 4 1 25 0 11 0 540003392 858800128 61088 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 61096 13073 16 0 209652 0 vsize: 838672 [startup+140.005 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15755 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 12505 52 4 1 25 0 11 0 540003392 858800128 64574 4294967295 134512640 134569956 3221224400 3221214912 1131420872 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 64574 13073 16 0 209652 0 vsize: 838672 [startup+150.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/63 15769 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 13400 53 4 2 25 0 10 0 540003392 858800128 68605 4294967295 134512640 134569956 3221224400 3221214392 1131275572 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 68605 13073 16 0 209652 0 vsize: 838672 [startup+160.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15784 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 14333 54 5 2 25 0 11 0 540003392 858800128 71153 4294967295 134512640 134569956 3221224400 3221214800 1131275653 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 71153 13073 16 0 209652 0 vsize: 838672 [startup+170.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15797 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 15228 55 5 2 25 0 11 0 540003392 858800128 75011 4294967295 134512640 134569956 3221224400 3221214968 1131440168 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 75011 13073 16 0 209652 0 vsize: 838672 [startup+180.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15810 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 16155 56 5 2 25 0 11 0 540003392 858800128 78446 4294967295 134512640 134569956 3221224400 3221214840 1131235954 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 78446 13073 16 0 209652 0 vsize: 838672 [startup+190.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15823 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 17085 56 6 2 25 0 11 0 540003392 858800128 80942 4294967295 134512640 134569956 3221224400 3221214800 1131275672 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 80942 13073 16 0 209652 0 vsize: 838672 [startup+200.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15835 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 18017 57 6 2 25 0 11 0 540003392 858800128 83437 4294967295 134512640 134569956 3221224400 3221214864 1131415729 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 83437 13073 16 0 209652 0 vsize: 838672 [startup+210.006 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15847 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 18948 57 6 2 25 0 11 0 540003392 858800128 85973 4294967295 134512640 134569956 3221224400 3221214992 1131441559 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 85973 13073 16 0 209652 0 vsize: 838672 [startup+220.008 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15858 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 19846 58 6 3 25 0 11 0 540003392 858800128 89857 4294967295 134512640 134569956 3221224400 3221214848 1131244468 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 89857 13073 16 0 209652 0 vsize: 838672 [startup+230.008 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15869 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 20766 59 6 3 25 0 11 0 540003392 858800128 98155 4294967295 134512640 134569956 3221224400 3221214912 1131420864 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 98155 13073 16 0 209652 0 vsize: 838672 [startup+240.011 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15880 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 21694 60 7 3 25 0 11 0 540003392 858800128 101072 4294967295 134512640 134569956 3221224400 3221214908 1131275552 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 101072 13073 16 0 209652 0 vsize: 838672 [startup+250.01 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15891 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 22623 61 7 3 25 0 11 0 540003392 858800128 103663 4294967295 134512640 134569956 3221224400 3221214912 1131420752 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 103663 13073 16 0 209652 0 vsize: 838672 [startup+260.01 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15901 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 23553 62 7 3 25 0 11 0 540003392 858800128 106290 4294967295 134512640 134569956 3221224400 3221214908 1131275552 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 106290 13073 16 0 209652 0 vsize: 838672 [startup+270.01 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15912 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 24520 62 8 3 25 0 11 0 540003392 858800128 107552 4294967295 134512640 134569956 3221224400 3221214912 1131420912 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 107552 13073 16 0 209652 0 vsize: 838672 [startup+280.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/63 15921 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 25450 63 8 3 25 0 10 0 540003392 858800128 110147 4294967295 134512640 134569956 3221224400 3221214472 1131313756 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 110147 13073 16 0 209652 0 vsize: 838672 [startup+290.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15931 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 26384 64 8 4 25 0 11 0 540003392 858800128 112643 4294967295 134512640 134569956 3221224400 3221214800 1131275680 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 112643 13073 16 0 209652 0 vsize: 838672 [startup+300.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15941 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 27313 64 9 4 25 0 11 0 540003392 858800128 115191 4294967295 134512640 134569956 3221224400 3221214800 1131276287 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 115191 13073 16 0 209652 0 vsize: 838672 [startup+310.02 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15950 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 28280 65 9 4 25 0 11 0 540003392 858800128 116499 4294967295 134512640 134569956 3221224400 3221214800 1131275626 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 116499 13073 16 0 209652 0 vsize: 838672 [startup+320.021 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15959 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 29212 66 9 4 25 0 11 0 540003392 858800128 118994 4294967295 134512640 134569956 3221224400 3221214912 1131420649 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 118994 13073 16 0 209652 0 vsize: 838672 [startup+330.031 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15968 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 30144 67 9 4 25 0 11 0 540003392 858800128 121490 4294967295 134512640 134569956 3221224400 3221214912 1131420733 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 121490 13073 16 0 209652 0 vsize: 838672 [startup+340.032 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15977 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 31111 67 10 4 25 0 11 0 540003392 858800128 122676 4294967295 134512640 134569956 3221224400 3221214864 1131415729 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 122676 13073 16 0 209652 0 vsize: 838672 [startup+350.032 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 15986 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 32043 68 10 4 25 0 11 0 540003392 858800128 125172 4294967295 134512640 134569956 3221224400 3221214912 1131420710 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 125172 13073 16 0 209652 0 vsize: 838672 [startup+360.034 s] Raw data (loadavg): 1.00 0.97 0.93 2/63 15994 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 32983 69 10 4 25 0 10 0 540003392 858800128 127724 4294967295 134512640 134569956 3221224400 3221213720 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 127727 13073 16 0 209652 0 vsize: 838672 [startup+370.035 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 16003 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 33937 70 10 4 25 0 11 0 540003392 858800128 129928 4294967295 134512640 134569956 3221224400 3221214800 1131276302 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 129928 13073 16 0 209652 0 vsize: 838672 [startup+380.036 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 16011 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 34884 71 10 5 25 0 11 0 540003392 858800128 131417 4294967295 134512640 134569956 3221224400 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 131443 13073 16 0 209652 0 vsize: 838672 [startup+390.036 s] Raw data (loadavg): 1.28 1.04 0.95 2/64 16020 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 35833 72 10 5 25 0 11 0 540003392 858800128 133786 4294967295 134512640 134569956 3221224400 3221214912 1131420752 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 133786 13073 16 0 209652 0 vsize: 838672 [startup+400.036 s] Raw data (loadavg): 1.24 1.04 0.95 2/63 16027 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 36765 73 11 5 25 0 10 0 540003392 858800128 136281 4294967295 134512640 134569956 3221224400 3221214504 1131334530 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 136281 13073 16 0 209652 0 vsize: 838672 [startup+410.036 s] Raw data (loadavg): 1.20 1.03 0.95 2/64 16036 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 37731 73 11 5 25 0 11 0 540003392 858800128 137470 4294967295 134512640 134569956 3221224400 3221214908 1131275552 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 137470 13073 16 0 209652 0 vsize: 838672 [startup+420.037 s] Raw data (loadavg): 1.17 1.03 0.95 2/64 16044 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 38695 74 11 5 25 0 11 0 540003392 858800128 138780 4294967295 134512640 134569956 3221224400 3221214800 1131275610 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 138780 13073 16 0 209652 0 vsize: 838672 [startup+430.038 s] Raw data (loadavg): 1.14 1.03 0.95 2/64 16051 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 39626 74 12 5 25 0 11 0 540003392 858800128 141277 4294967295 134512640 134569956 3221224400 3221214848 1131244468 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 141277 13073 16 0 209652 0 vsize: 838672 [startup+440.037 s] Raw data (loadavg): 1.12 1.03 0.95 2/64 16059 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 40592 75 12 5 25 0 11 0 540003392 858800128 142464 4294967295 134512640 134569956 3221224400 3221214912 1131420752 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 142464 13073 16 0 209652 0 vsize: 838672 [startup+450.037 s] Raw data (loadavg): 1.10 1.03 0.95 2/64 16067 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 41526 76 12 5 25 0 11 0 540003392 858800128 144907 4294967295 134512640 134569956 3221224400 3221214908 1131276315 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 144907 13073 16 0 209652 0 vsize: 838672 [startup+460.037 s] Raw data (loadavg): 1.09 1.03 0.95 2/64 16074 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 42492 76 12 5 25 0 11 0 540003392 858800128 146137 4294967295 134512640 134569956 3221224400 3221214912 1131420718 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 146137 13073 16 0 209652 0 vsize: 838672 [startup+470.038 s] Raw data (loadavg): 1.07 1.03 0.95 2/64 16082 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 43456 77 12 5 25 0 11 0 540003392 858800128 147403 4294967295 134512640 134569956 3221224400 3221214912 1131420752 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 147403 13073 16 0 209652 0 vsize: 838672 [startup+480.038 s] Raw data (loadavg): 1.06 1.02 0.95 2/64 16089 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 44387 78 12 5 25 0 11 0 540003392 858800128 149900 4294967295 134512640 134569956 3221224400 3221214800 1131275689 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 149900 13073 16 0 209652 0 vsize: 838672 [startup+490.037 s] Raw data (loadavg): 1.05 1.02 0.95 2/64 16096 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 45353 79 13 5 25 0 11 0 540003392 858800128 151101 4294967295 134512640 134569956 3221224400 3221214800 1131275666 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 151101 13073 16 0 209652 0 vsize: 838672 [startup+500.038 s] Raw data (loadavg): 1.04 1.02 0.95 2/64 16103 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 46311 79 13 6 25 0 11 0 540003392 858800128 152422 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 152422 13073 16 0 209652 0 vsize: 838672 [startup+510.038 s] Raw data (loadavg): 1.04 1.02 0.95 2/63 16110 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 47255 80 13 6 25 0 10 0 540003392 858800128 154692 4294967295 134512640 134569956 3221224400 3221214924 1076461336 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 154692 13073 16 0 209652 0 vsize: 838672 [startup+520.038 s] Raw data (loadavg): 1.03 1.02 0.95 2/64 16117 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 48197 81 13 6 25 0 11 0 540003392 858800128 157188 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 157188 13073 16 0 209652 0 vsize: 838672 [startup+530.038 s] Raw data (loadavg): 1.02 1.02 0.95 2/64 16117 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 48250 81 13 6 25 0 11 0 540003392 858800128 157195 4294967295 134512640 134569956 3221224400 3221213664 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 157195 13073 16 0 209652 0 vsize: 838672 [startup+540.038 s] Raw data (loadavg): 1.02 1.02 0.95 2/64 16119 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 48497 82 13 6 25 0 11 0 540003392 858800128 160662 4294967295 134512640 134569956 3221224400 3221214912 1131420789 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 160662 13073 16 0 209652 0 vsize: 838672 [startup+550.038 s] Raw data (loadavg): 1.02 1.02 0.95 2/63 16122 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 48949 82 13 6 25 0 10 0 540003392 858800128 160662 4294967295 134512640 134569956 3221224400 3221213272 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 160662 13073 16 0 209652 0 vsize: 838672 [startup+560.038 s] Raw data (loadavg): 1.01 1.02 0.95 2/64 16124 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 49189 82 14 6 25 0 11 0 540003392 858800128 162085 4294967295 134512640 134569956 3221224400 3221214912 1131420752 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 162085 13073 16 0 209652 0 vsize: 838672 [startup+570.038 s] Raw data (loadavg): 1.01 1.02 0.95 2/64 16128 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 49772 83 14 6 25 0 11 0 540003392 858800128 162085 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 162085 13073 16 0 209652 0 vsize: 838672 [startup+580.039 s] Raw data (loadavg): 1.01 1.02 0.95 2/64 16129 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 49872 83 14 6 25 0 11 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221214800 1131275672 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+590.038 s] Raw data (loadavg): 1.01 1.01 0.95 2/63 16133 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 50479 83 14 6 25 0 10 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+600.038 s] Raw data (loadavg): 1.01 1.01 0.95 2/63 16133 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 50479 83 14 6 25 0 10 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+610.038 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16137 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 50927 84 14 6 25 0 11 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221214912 1131420824 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+620.038 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16139 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 51317 84 14 6 25 0 11 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+630.038 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16141 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 51583 84 14 6 25 0 11 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221214912 1131420804 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+640.039 s] Raw data (loadavg): 1.00 1.01 0.95 2/63 16144 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 52034 84 14 6 25 0 10 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+650.041 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16146 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 52223 84 14 6 25 0 11 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221214912 1131420785 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+660.04 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16150 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 52882 85 14 6 25 0 11 0 540003392 858800128 163338 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163338 13073 16 0 209652 0 vsize: 838672 [startup+670.041 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16150 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 52882 85 14 6 25 0 11 0 540003392 858800128 163340 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 163340 13073 16 0 209652 0 vsize: 838672 [startup+680.042 s] Raw data (loadavg): 1.00 1.01 0.95 2/64 16155 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 53615 85 14 6 25 0 11 0 540003392 858800128 164672 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 164672 13073 16 0 209652 0 vsize: 838672 [startup+690.042 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16155 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 53615 85 14 6 25 0 11 0 540003392 858800128 164673 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 164673 13073 16 0 209652 0 vsize: 838672 [startup+700.042 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16160 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 54350 86 14 6 25 0 10 0 540003392 858800128 165142 4294967295 134512640 134569956 3221224400 3221213264 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 165142 13073 16 0 209652 0 vsize: 838672 [startup+710.043 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16160 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 54350 86 14 6 25 0 10 0 540003392 858800128 165145 4294967295 134512640 134569956 3221224400 3221213264 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 165145 13073 16 0 209652 0 vsize: 838672 [startup+720.043 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16165 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 55048 87 14 6 25 0 11 0 540003392 858800128 166646 4294967295 134512640 134569956 3221224400 3221214912 1131420740 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 166646 13073 16 0 209652 0 vsize: 838672 [startup+730.043 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16166 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 55216 87 14 7 25 0 11 0 540003392 858800128 166646 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 166646 13073 16 0 209652 0 vsize: 838672 [startup+740.043 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16169 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 55639 87 14 7 25 0 11 0 540003392 858800128 168003 4294967295 134512640 134569956 3221224400 3221214912 1131420872 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 168003 13073 16 0 209652 0 vsize: 838672 [startup+750.043 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16171 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 55969 87 14 7 25 0 10 0 540003392 858800128 168003 4294967295 134512640 134569956 3221224400 3221214108 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 168003 13073 16 0 209652 0 vsize: 838672 [startup+760.044 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16173 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 56219 87 14 7 25 0 11 0 540003392 858800128 169198 4294967295 134512640 134569956 3221224400 3221214908 1131275552 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 169198 13073 16 0 209652 0 vsize: 838672 [startup+770.044 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16177 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 56848 88 14 7 25 0 11 0 540003392 858800128 169198 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 169198 13073 16 0 209652 0 vsize: 838672 [startup+780.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16177 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 56848 88 14 7 25 0 11 0 540003392 858800128 169200 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 169200 13073 16 0 209652 0 vsize: 838672 [startup+790.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16182 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 57608 89 14 7 25 0 10 0 540003392 858800128 170132 4294967295 134512640 134569956 3221224400 3221213400 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 170132 13073 16 0 209652 0 vsize: 838672 [startup+800.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16182 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 57608 89 14 7 25 0 10 0 540003392 858800128 170134 4294967295 134512640 134569956 3221224400 3221213400 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 170134 13073 16 0 209652 0 vsize: 838672 [startup+810.044 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16187 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 58319 89 15 7 25 0 11 0 540003392 858800128 171383 4294967295 134512640 134569956 3221224400 3221214800 1131275616 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 171383 13073 16 0 209652 0 vsize: 838672 [startup+820.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16188 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18017 3 1 0 58504 89 15 7 25 0 11 0 540003392 858800128 171383 4294967295 134512640 134569956 3221224400 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171383 13073 16 0 209652 0 vsize: 838672 [startup+830.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16191 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18017 3 1 0 58862 89 15 7 25 0 11 0 540003392 858800128 171452 4294967295 134512640 134569956 3221224400 3221214800 1131275672 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171452 13073 16 0 209652 0 vsize: 838672 [startup+840.044 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16193 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 59360 90 15 7 16 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213264 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+850.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16194 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 59372 90 15 7 18 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214912 1131420905 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+860.045 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16198 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 60207 90 15 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+870.046 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16198 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 60207 90 15 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+880.046 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16199 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 60302 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214912 1131420752 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+890.046 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16203 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 61046 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+900.046 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16203 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 61046 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+910.046 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16207 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 61760 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+920.047 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16207 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 61760 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+930.046 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16211 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 62315 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214912 1131420733 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+940.047 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16211 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 62477 91 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213560 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+950.048 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16214 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 62812 92 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214912 1131420730 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+960.048 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16215 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 63175 92 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+970.049 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16215 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 63175 92 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+980.049 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16218 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 63706 92 15 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214064 1079948887 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+990.049 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16218 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 63739 92 15 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213264 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1000.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16221 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 64186 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214088 1076874300 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1010.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16221 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 64292 93 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1020.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16224 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 64664 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214800 1131275680 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1030.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16224 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 64853 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213360 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1040.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16226 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 65141 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214800 1131275577 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1050.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16227 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 65352 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213560 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1060.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16229 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 65612 93 16 7 19 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214912 1131420912 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1070.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16229 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 65811 93 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1080.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16231 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 66080 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214720 1131248020 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1090.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16231 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 66218 93 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213296 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1100.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16233 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 66543 93 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214080 1077371573 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1110.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16233 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 66625 93 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1120.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16235 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 67006 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214092 1077100787 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1130.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16235 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 67034 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213376 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1140.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16235 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 67034 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213376 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1150.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16237 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 67424 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1160.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16237 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 67424 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1170.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16238 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 67679 94 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1180.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16239 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 67803 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214800 1131275591 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1190.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16240 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 68064 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1200.05 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16241 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 68259 94 16 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214304 1076461292 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1210.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16241 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 68320 94 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1220.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16242 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 68564 95 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1230.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16242 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 68564 95 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1240.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16243 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 68807 95 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213296 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1250.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16243 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 68807 95 16 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213296 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1260.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16244 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69048 95 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213272 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1270.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16244 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69048 95 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213272 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1280.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16245 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69289 95 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213264 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1290.06 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16246 Raw data (stat): 15594 (java) R 15593 27222 27221 0 -1 0 18021 3 1 0 69489 95 17 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221214848 1131244520 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1300.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16246 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69536 95 17 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1310.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16247 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69775 95 17 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1320.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16247 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69775 95 17 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1330.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16248 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69979 96 17 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213424 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1340.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/64 16248 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 69979 96 17 7 25 0 11 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213424 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1350.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16248 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 70101 96 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1360.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16248 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 70101 96 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1370.07 s] Raw data (loadavg): 1.00 1.00 0.95 2/63 16248 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 70101 96 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 838672 [startup+1374.49 s] Raw data (loadavg): 1.00 1.00 0.95 1/53 16248 Raw data (stat): 15594 (java) S 15593 27222 27221 0 -1 0 18021 3 1 0 70101 96 17 7 25 0 10 0 540003392 858800128 171456 4294967295 134512640 134569956 3221224400 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209668 171456 13073 16 0 209652 0 vsize: 0 Child status: 1 Real time (s): 1374.49 CPU time (s): 1377.64 CPU user time (s): 1373.19 CPU system time (s): 4.44732 CPU usage (%): 100.229 Max. virtual memory (Kb): 838672 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####