Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-grow22.opb |
MD5SUM | 252426e4d147311f236e947ac8e9f53d |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1958 |
Biggest coefficient in the objective function | 3758096384 |
Number of bits for the biggest coefficient in the objective function | 32 |
Sum of the numbers in the objective function | 234612588283 |
Number of bits of the sum of numbers in the objective function | 38 |
Biggest number in a constraint | 878188741787648 |
Number of bits of the biggest number in a constraint | 50 |
Biggest sum of numbers in a constraint | 4550739094651140 |
Number of bits of the biggest sum of numbers | 53 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1264.78 |
Number of variables | 25124 |
Total number of constraints | 1320 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1320 |
Minimum length of a constraint | 22 |
Maximum length of a constraint | 491 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-04-21 10:14:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=10916 boxname=wulflinc20 idbench=840 idsolver=9 numberseed=0 MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac /oldhome/oroussel/solvers/sat4jPseudo.jar MD5SUM BENCH: 252426e4d147311f236e947ac8e9f53d /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-grow22.opb REAL COMMAND: java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-grow22.opb IDLAUNCH: 10916 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 396360 kB Buffers: 24968 kB Cached: 588624 kB SwapCached: 516 kB Active: 125472 kB Inactive: 490112 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 396108 kB SwapTotal: 2097892 kB SwapFree: 2096480 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5116 kB Slab: 17152 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 10:35:31 (client local time) WITH STATUS 143 IN 1279.22 SECONDS stats: 10916 7 1279.22 143 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c solving /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-grow22.opb c reading problem c [nbvar=25124] c [nbconstr=1320] c time 185.327 c #vars 25124 c #clauses 1761 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=0 c Current CPU time (ms) : 193.821 c starts : 1 c conflicts : 0 c decisions : 24332 c propagations : 25124 c inspects : 27638 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=-1879048192 c Current CPU time (ms) : 196.108 c starts : 2 c conflicts : 0 c decisions : 48663 c propagations : 50248 c inspects : 30063 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=1476395008 c Current CPU time (ms) : 198.498 c starts : 3 c conflicts : 0 c decisions : 72993 c propagations : 75372 c inspects : 32497 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=1476395008 c Current CPU time (ms) : 200.953 c starts : 4 c conflicts : 0 c decisions : 97323 c propagations : 100496 c inspects : 34924 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=1476395008 c Current CPU time (ms) : 203.35 c starts : 5 c conflicts : 0 c decisions : 121653 c propagations : 125620 c inspects : 37355 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=1476395008 c Current CPU time (ms) : 205.815 c starts : 6 c conflicts : 0 c decisions : 145983 c propagations : 150744 c inspects : 39784 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=1476395008 c Current CPU time (ms) : 208.221 c starts : 7 c conflicts : 0 c decisions : 170313 c propagations : 175868 c inspects : 42214 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=1476395008 c Current CPU time (ms) : 210.578 c starts : 8 c conflicts : 0 c decisions : 194643 c propagations : 200992 c inspects : 44642 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=1476395008 c Current CPU time (ms) : 213.102 c starts : 9 c conflicts : 0 c decisions : 218973 c propagations : 226116 c inspects : 47072 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=1476395008 c Current CPU time (ms) : 215.508 c starts : 10 c conflicts : 0 c decisions : 243303 c propagations : 251240 c inspects : 49499 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=1476395008 c Current CPU time (ms) : 217.976 c starts : 11 c conflicts : 0 c decisions : 267633 c propagations : 276364 c inspects : 51925 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=1476395008 c Current CPU time (ms) : 220.381 c starts : 12 c conflicts : 0 c decisions : 291963 c propagations : 301488 c inspects : 54355 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=1476395008 c Current CPU time (ms) : 222.782 c starts : 13 c conflicts : 0 c decisions : 316293 c propagations : 326612 c inspects : 56782 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=1476395008 c Current CPU time (ms) : 225.22 c starts : 14 c conflicts : 0 c decisions : 340623 c propagations : 351736 c inspects : 59213 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=1476395008 c Current CPU time (ms) : 227.586 c starts : 15 c conflicts : 0 c decisions : 364953 c propagations : 376860 c inspects : 61639 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=1476395008 c Current CPU time (ms) : 230.045 c starts : 16 c conflicts : 0 c decisions : 389283 c propagations : 401984 c inspects : 64067 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=1476395008 c Current CPU time (ms) : 232.463 c starts : 17 c conflicts : 0 c decisions : 413613 c propagations : 427108 c inspects : 66494 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=1476395008 c Current CPU time (ms) : 234.802 c starts : 18 c conflicts : 0 c decisions : 437943 c propagations : 452232 c inspects : 68923 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=1476395008 c Current CPU time (ms) : 237.164 c starts : 19 c conflicts : 0 c decisions : 462273 c propagations : 477356 c inspects : 71349 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=1476395008 c Current CPU time (ms) : 239.459 c starts : 20 c conflicts : 0 c decisions : 486603 c propagations : 502480 c inspects : 73778 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=1476395008 c Current CPU time (ms) : 241.79 c starts : 21 c conflicts : 0 c decisions : 510933 c propagations : 527604 c inspects : 76204 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=1476395008 c Current CPU time (ms) : 244.098 c starts : 22 c conflicts : 0 c decisions : 535263 c propagations : 552728 c inspects : 78634 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=1476395008 c Current CPU time (ms) : 246.427 c starts : 23 c conflicts : 0 c decisions : 559593 c propagations : 577852 c inspects : 81061 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=1476395008 c Current CPU time (ms) : 248.776 c starts : 24 c conflicts : 0 c decisions : 583923 c propagations : 602976 c inspects : 83489 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=1476395008 c Current CPU time (ms) : 251.115 c starts : 25 c conflicts : 0 c decisions : 608253 c propagations : 628100 c inspects : 85916 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=1476395008 c Current CPU time (ms) : 253.457 c starts : 26 c conflicts : 0 c decisions : 632583 c propagations : 653224 c inspects : 88344 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=1476395008 c Current CPU time (ms) : 255.858 c starts : 27 c conflicts : 0 c decisions : 656913 c propagations : 678348 c inspects : 90769 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=1476395008 c Current CPU time (ms) : 258.216 c starts : 28 c conflicts : 0 c decisions : 681243 c propagations : 703472 c inspects : 93194 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=1476395008 c Current CPU time (ms) : 260.634 c starts : 29 c conflicts : 0 c decisions : 705573 c propagations : 728596 c inspects : 95623 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=1476395008 c Current CPU time (ms) : 263.002 c starts : 30 c conflicts : 0 c decisions : 729903 c propagations : 753720 c inspects : 98053 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=1476395008 c Current CPU time (ms) : 265.38 c starts : 31 c conflicts : 0 c decisions : 754233 c propagations : 778844 c inspects : 100483 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=1476395008 c Current CPU time (ms) : 267.856 c starts : 32 c conflicts : 0 c decisions : 778563 c propagations : 803968 c inspects : 102911 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=1476395008 c Current CPU time (ms) : 270.325 c starts : 33 c conflicts : 0 c decisions : 802893 c propagations : 829092 c inspects : 105342 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=1476395008 c Current CPU time (ms) : 272.616 c starts : 34 c conflicts : 0 c decisions : 827223 c propagations : 854216 c inspects : 107770 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=1476395008 c Current CPU time (ms) : 274.93 c starts : 35 c conflicts : 0 c decisions : 851553 c propagations : 879340 c inspects : 110199 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=1476395008 c Current CPU time (ms) : 277.229 c starts : 36 c conflicts : 0 c decisions : 875883 c propagations : 904464 c inspects : 112628 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=1476395008 c Current CPU time (ms) : 279.537 c starts : 37 c conflicts : 0 c decisions : 900213 c propagations : 929588 c inspects : 115056 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=1476395008 c Current CPU time (ms) : 281.831 c starts : 38 c conflicts : 0 c decisions : 924543 c propagations : 954712 c inspects : 117487 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=1476395008 c Current CPU time (ms) : 284.194 c starts : 39 c conflicts : 0 c decisions : 948873 c propagations : 979836 c inspects : 119917 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=1476395008 c Current CPU time (ms) : 286.483 c starts : 40 c conflicts : 0 c decisions : 973203 c propagations : 1004960 c inspects : 122346 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=1476395008 c Current CPU time (ms) : 288.793 c starts : 41 c conflicts : 0 c decisions : 997533 c propagations : 1030084 c inspects : 124777 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=1476395008 c Current CPU time (ms) : 291.148 c starts : 42 c conflicts : 0 c decisions : 1021863 c propagations : 1055208 c inspects : 127206 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=1476395008 c Current CPU time (ms) : 293.497 c starts : 43 c conflicts : 0 c decisions : 1046193 c propagations : 1080332 c inspects : 129632 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=1476395008 c Current CPU time (ms) : 295.908 c starts : 44 c conflicts : 0 c decisions : 1070523 c propagations : 1105456 c inspects : 132059 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=1476395008 c Current CPU time (ms) : 298.268 c starts : 45 c conflicts : 0 c decisions : 1094853 c propagations : 1130580 c inspects : 134486 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=1476395008 c Current CPU time (ms) : 300.646 c starts : 46 c conflicts : 0 c decisions : 1119183 c propagations : 1155704 c inspects : 136914 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=1476395008 c Current CPU time (ms) : 303.066 c starts : 47 c conflicts : 0 c decisions : 1143513 c propagations : 1180828 c inspects : 139344 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=1476395008 c Current CPU time (ms) : 305.451 c starts : 48 c conflicts : 0 c decisions : 1167843 c propagations : 1205952 c inspects : 141773 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=1476395008 c Current CPU time (ms) : 307.834 c starts : 49 c conflicts : 0 c decisions : 1192173 c propagations : 1231076 c inspects : 144204 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=1476395008 c Current CPU time (ms) : 310.243 c starts : 50 c conflicts : 0 c decisions : 1216503 c propagations : 1256200 c inspects : 146632 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=1476395008 c Current CPU time (ms) : 312.598 c starts : 51 c conflicts : 0 c decisions : 1240833 c propagations : 1281324 c inspects : 149060 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=1476395008 c Current CPU time (ms) : 315.03 c starts : 52 c conflicts : 0 c decisions : 1265163 c propagations : 1306448 c inspects : 151487 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=1476395008 c Current CPU time (ms) : 317.385 c starts : 53 c conflicts : 0 c decisions : 1289493 c propagations : 1331572 c inspects : 153915 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=1476395008 c Current CPU time (ms) : 319.752 c starts : 54 c conflicts : 0 c decisions : 1313823 c propagations : 1356696 c inspects : 156342 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=1476395008 c Current CPU time (ms) : 322.162 c starts : 55 c conflicts : 0 c decisions : 1338153 c propagations : 1381820 c inspects : 158770 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=1476395008 c Current CPU time (ms) : 324.536 c starts : 56 c conflicts : 0 c decisions : 1362483 c propagations : 1406944 c inspects : 161197 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=1476395008 c Current CPU time (ms) : 326.948 c starts : 57 c conflicts : 0 c decisions : 1386813 c propagations : 1432068 c inspects : 163623 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=1476395008 c Current CPU time (ms) : 329.298 c starts : 58 c conflicts : 0 c decisions : 1411143 c propagations : 1457192 c inspects : 166053 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=1476395008 c Current CPU time (ms) : 331.651 c starts : 59 c conflicts : 0 c decisions : 1435473 c propagations : 1482316 c inspects : 168484 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=1476395008 c Current CPU time (ms) : 334.085 c starts : 60 c conflicts : 0 c decisions : 1459803 c propagations : 1507440 c inspects : 170911 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=1476395008 c Current CPU time (ms) : 336.443 c starts : 61 c conflicts : 0 c decisions : 1484133 c propagations : 1532564 c inspects : 173341 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=1476395008 c Current CPU time (ms) : 338.794 c starts : 62 c conflicts : 0 c decisions : 1508463 c propagations : 1557688 c inspects : 175768 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=1476395008 c Current CPU time (ms) : 341.198 c starts : 63 c conflicts : 0 c decisions : 1532793 c propagations : 1582812 c inspects : 178197 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=1476395008 c Current CPU time (ms) : 343.649 c starts : 64 c conflicts : 0 c decisions : 1557123 c propagations : 1607936 c inspects : 180628 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=1476395008 c Current CPU time (ms) : 346.188 c starts : 65 c conflicts : 0 c decisions : 1581453 c propagations : 1633060 c inspects : 183059 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=1476395008 c Current CPU time (ms) : 348.535 c starts : 66 c conflicts : 0 c decisions : 1605783 c propagations : 1658184 c inspects : 185489 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=1476395008 c Current CPU time (ms) : 350.978 c starts : 67 c conflicts : 0 c decisions : 1630113 c propagations : 1683308 c inspects : 187918 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=1476395008 c Current CPU time (ms) : 353.329 c starts : 68 c conflicts : 0 c decisions : 1654443 c propagations : 1708432 c inspects : 190346 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=1476395008 c Current CPU time (ms) : 355.725 c starts : 69 c conflicts : 0 c decisions : 1678773 c propagations : 1733556 c inspects : 192775 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=1476395008 c Current CPU time (ms) : 358.125 c starts : 70 c conflicts : 0 c decisions : 1703103 c propagations : 1758680 c inspects : 195204 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=1476395008 c Current CPU time (ms) : 360.491 c starts : 71 c conflicts : 0 c decisions : 1727433 c propagations : 1783804 c inspects : 197632 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=1476395008 c Current CPU time (ms) : 362.9 c starts : 72 c conflicts : 0 c decisions : 1751763 c propagations : 1808928 c inspects : 200059 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=1476395008 c Current CPU time (ms) : 365.248 c starts : 73 c conflicts : 0 c decisions : 1776093 c propagations : 1834052 c inspects : 202488 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=1476395008 c Current CPU time (ms) : 367.612 c starts : 74 c conflicts : 0 c decisions : 1800423 c propagations : 1859176 c inspects : 204917 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=1476395008 c Current CPU time (ms) : 370.055 c starts : 75 c conflicts : 0 c decisions : 1824753 c propagations : 1884300 c inspects : 207343 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=1476395008 c Current CPU time (ms) : 372.407 c starts : 76 c conflicts : 0 c decisions : 1849083 c propagations : 1909424 c inspects : 209769 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=1476395008 c Current CPU time (ms) : 374.8 c starts : 77 c conflicts : 0 c decisions : 1873413 c propagations : 1934548 c inspects : 212198 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=1476395008 c Current CPU time (ms) : 377.219 c starts : 78 c conflicts : 0 c decisions : 1897743 c propagations : 1959672 c inspects : 214624 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=1476395008 c Current CPU time (ms) : 379.592 c starts : 79 c conflicts : 0 c decisions : 1922073 c propagations : 1984796 c inspects : 217054 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=1476395008 c Current CPU time (ms) : 381.989 c starts : 80 c conflicts : 0 c decisions : 1946403 c propagations : 2009920 c inspects : 219481 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=1476395008 c Current CPU time (ms) : 384.387 c starts : 81 c conflicts : 0 c decisions : 1970733 c propagations : 2035044 c inspects : 221911 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=1476395008 c Current CPU time (ms) : 386.735 c starts : 82 c conflicts : 0 c decisions : 1995063 c propagations : 2060168 c inspects : 224338 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=1476395008 c Current CPU time (ms) : 389.136 c starts : 83 c conflicts : 0 c decisions : 2019393 c propagations : 2085292 c inspects : 226765 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=1476395008 c Current CPU time (ms) : 391.528 c starts : 84 c conflicts : 0 c decisions : 2043723 c propagations : 2110416 c inspects : 229192 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=1476395008 c Current CPU time (ms) : 393.932 c starts : 85 c conflicts : 0 c decisions : 2068053 c propagations : 2135540 c inspects : 231623 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=1476395008 c Current CPU time (ms) : 396.298 c starts : 86 c conflicts : 0 c decisions : 2092383 c propagations : 2160664 c inspects : 234051 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=1476395008 c Current CPU time (ms) : 398.649 c starts : 87 c conflicts : 0 c decisions : 2116713 c propagations : 2185788 c inspects : 236479 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=1476395008 c Current CPU time (ms) : 401.08 c starts : 88 c conflicts : 0 c decisions : 2141043 c propagations : 2210912 c inspects : 238908 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=1476395008 c Current CPU time (ms) : 403.477 c starts : 89 c conflicts : 0 c decisions : 2165373 c propagations : 2236036 c inspects : 241336 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=1476395008 c Current CPU time (ms) : 405.861 c starts : 90 c conflicts : 0 c decisions : 2189703 c propagations : 2261160 c inspects : 243765 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=1476395008 c Current CPU time (ms) : 408.29 c starts : 91 c conflicts : 0 c decisions : 2214033 c propagations : 2286284 c inspects : 246194 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=1476395008 c Current CPU time (ms) : 410.633 c starts : 92 c conflicts : 0 c decisions : 2238363 c propagations : 2311408 c inspects : 248623 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=1476395008 c Current CPU time (ms) : 413.03 c starts : 93 c conflicts : 0 c decisions : 2262693 c propagations : 2336532 c inspects : 251051 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=1476395008 c Current CPU time (ms) : 415.394 c starts : 94 c conflicts : 0 c decisions : 2287023 c propagations : 2361656 c inspects : 253479 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=1476395008 c Current CPU time (ms) : 417.744 c starts : 95 c conflicts : 0 c decisions : 2311353 c propagations : 2386780 c inspects : 255908 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=1476395008 c Current CPU time (ms) : 420.139 c starts : 96 c conflicts : 0 c decisions : 2335683 c propagations : 2411904 c inspects : 258337 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=1476395008 c Current CPU time (ms) : 422.538 c starts : 97 c conflicts : 0 c decisions : 2360013 c propagations : 2437028 c inspects : 260766 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=1476395008 c Current CPU time (ms) : 424.963 c starts : 98 c conflicts : 0 c decisions : 2384343 c propagations : 2462152 c inspects : 263193 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=1476395008 c Current CPU time (ms) : 427.366 c starts : 99 c conflicts : 0 c decisions : 2408673 c propagations : 2487276 c inspects : 265622 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=1476395008 c Current CPU time (ms) : 429.757 c starts : 100 c conflicts : 0 c decisions : 2433003 c propagations : 2512400 c inspects : 268052 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=1476395008 c Current CPU time (ms) : 432.191 c starts : 101 c conflicts : 0 c decisions : 2457333 c propagations : 2537524 c inspects : 270482 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=1476395008 c Current CPU time (ms) : 434.557 c starts : 102 c conflicts : 0 c decisions : 2481663 c propagations : 2562648 c inspects : 272912 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=1476395008 c Current CPU time (ms) : 436.953 c starts : 103 c conflicts : 0 c decisions : 2505993 c propagations : 2587772 c inspects : 275340 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=1476395008 c Current CPU time (ms) : 439.38 c starts : 104 c conflicts : 0 c decisions : 2530323 c propagations : 2612896 c inspects : 277766 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=1476395008 c Current CPU time (ms) : 441.754 c starts : 105 c conflicts : 0 c decisions : 2554653 c propagations : 2638020 c inspects : 280193 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=1476395008 c Current CPU time (ms) : 444.18 c starts : 106 c conflicts : 0 c decisions : 2578983 c propagations : 2663144 c inspects : 282620 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=1476395008 c Current CPU time (ms) : 446.599 c starts : 107 c conflicts : 0 c decisions : 2603313 c propagations : 2688268 c inspects : 285048 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=1476395008 c Current CPU time (ms) : 448.976 c starts : 108 c conflicts : 0 c decisions : 2627643 c propagations : 2713392 c inspects : 287476 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=1476395008 c Current CPU time (ms) : 451.413 c starts : 109 c conflicts : 0 c decisions : 2651973 c propagations : 2738516 c inspects : 289909 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=1476395008 c Current CPU time (ms) : 453.818 c starts : 110 c conflicts : 0 c decisions : 2676303 c propagations : 2763640 c inspects : 292336 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=1476395008 c Current CPU time (ms) : 456.235 c starts : 111 c conflicts : 0 c decisions : 2700633 c propagations : 2788764 c inspects : 294764 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=1476395008 c Current CPU time (ms) : 458.613 c starts : 112 c conflicts : 0 c decisions : 2724963 c propagations : 2813888 c inspects : 297193 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=1476395008 c Current CPU time (ms) : 460.98 c starts : 113 c conflicts : 0 c decisions : 2749293 c propagations : 2839012 c inspects : 299622 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=1476395008 c Current CPU time (ms) : 463.377 c starts : 114 c conflicts : 0 c decisions : 2773623 c propagations : 2864136 c inspects : 302051 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=1476395008 c Current CPU time (ms) : 465.727 c starts : 115 c conflicts : 0 c decisions : 2797953 c propagations : 2889260 c inspects : 304479 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=1476395008 c Current CPU time (ms) : 468.103 c starts : 116 c conflicts : 0 c decisions : 2822283 c propagations : 2914384 c inspects : 306909 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=1476395008 c Current CPU time (ms) : 470.533 c starts : 117 c conflicts : 0 c decisions : 2846613 c propagations : 2939508 c inspects : 309340 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=1476395008 c Current CPU time (ms) : 472.882 c starts : 118 c conflicts : 0 c decisions : 2870943 c propagations : 2964632 c inspects : 311769 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=1476395008 c Current CPU time (ms) : 475.292 c starts : 119 c conflicts : 0 c decisions : 2895273 c propagations : 2989756 c inspects : 314200 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=1476395008 c Current CPU time (ms) : 477.664 c starts : 120 c conflicts : 0 c decisions : 2919603 c propagations : 3014880 c inspects : 316628 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=1476395008 c Current CPU time (ms) : 480.046 c starts : 121 c conflicts : 0 c decisions : 2943933 c propagations : 3040004 c inspects : 319057 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=1476395008 c Current CPU time (ms) : 482.454 c starts : 122 c conflicts : 0 c decisions : 2968263 c propagations : 3065128 c inspects : 321485 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=1476395008 c Current CPU time (ms) : 484.854 c starts : 123 c conflicts : 0 c decisions : 2992593 c propagations : 3090252 c inspects : 323912 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=1476395008 c Current CPU time (ms) : 487.261 c starts : 124 c conflicts : 0 c decisions : 3016923 c propagations : 3115376 c inspects : 326336 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=1476395008 c Current CPU time (ms) : 489.646 c starts : 125 c conflicts : 0 c decisions : 3041253 c propagations : 3140500 c inspects : 328765 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=1476395008 c Current CPU time (ms) : 492.021 c starts : 126 c conflicts : 0 c decisions : 3065583 c propagations : 3165624 c inspects : 331194 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=1476395008 c Current CPU time (ms) : 494.429 c starts : 127 c conflicts : 0 c decisions : 3089913 c propagations : 3190748 c inspects : 333621 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=1476395008 c Current CPU time (ms) : 497.036 c starts : 128 c conflicts : 0 c decisions : 3114243 c propagations : 3215872 c inspects : 336049 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=1476395008 c Current CPU time (ms) : 499.7 c starts : 129 c conflicts : 0 c decisions : 3138573 c propagations : 3240996 c inspects : 338477 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=1476395008 c Current CPU time (ms) : 502.086 c starts : 130 c conflicts : 0 c decisions : 3162903 c propagations : 3266120 c inspects : 340904 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=1476395008 c Current CPU time (ms) : 504.513 c starts : 131 c conflicts : 0 c decisions : 3187233 c propagations : 3291244 c inspects : 343332 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=1476395008 c Current CPU time (ms) : 506.934 c starts : 132 c conflicts : 0 c decisions : 3211563 c propagations : 3316368 c inspects : 345759 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=1476395008 c Current CPU time (ms) : 509.276 c starts : 133 c conflicts : 0 c decisions : 3235893 c propagations : 3341492 c inspects : 348189 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=1476395008 c Current CPU time (ms) : 511.669 c starts : 134 c conflicts : 0 c decisions : 3260223 c propagations : 3366616 c inspects : 350617 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=1476395008 c Current CPU time (ms) : 514.029 c starts : 135 c conflicts : 0 c decisions : 3284553 c propagations : 3391740 c inspects : 353047 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=1476395008 c Current CPU time (ms) : 516.529 c starts : 136 c conflicts : 0 c decisions : 3308883 c propagations : 3416864 c inspects : 355474 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=1476395008 c Current CPU time (ms) : 518.855 c starts : 137 c conflicts : 0 c decisions : 3333213 c propagations : 3441988 c inspects : 357904 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=1476395008 c Current CPU time (ms) : 521.192 c starts : 138 c conflicts : 0 c decisions : 3357543 c propagations : 3467112 c inspects : 360333 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=1476395008 c Current CPU time (ms) : 523.586 c starts : 139 c conflicts : 0 c decisions : 3381873 c propagations : 3492236 c inspects : 362762 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=1476395008 c Current CPU time (ms) : 526.011 c starts : 140 c conflicts : 0 c decisions : 3406203 c propagations : 3517360 c inspects : 365190 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=1476395008 c Current CPU time (ms) : 528.5 c starts : 141 c conflicts : 0 c decisions : 3430533 c propagations : 3542484 c inspects : 367615 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=1476395008 c Current CPU time (ms) : 530.839 c starts : 142 c conflicts : 0 c decisions : 3454863 c propagations : 3567608 c inspects : 370043 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=1476395008 c Current CPU time (ms) : 533.194 c starts : 143 c conflicts : 0 c decisions : 3479193 c propagations : 3592732 c inspects : 372471 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=1476395008 c Current CPU time (ms) : 535.568 c starts : 144 c conflicts : 0 c decisions : 3503523 c propagations : 3617856 c inspects : 374898 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=1476395008 c Current CPU time (ms) : 537.918 c starts : 145 c conflicts : 0 c decisions : 3527853 c propagations : 3642980 c inspects : 377325 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=1476395008 c Current CPU time (ms) : 540.259 c starts : 146 c conflicts : 0 c decisions : 3552183 c propagations : 3668104 c inspects : 379755 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=1476395008 c Current CPU time (ms) : 542.734 c starts : 147 c conflicts : 0 c decisions : 3576513 c propagations : 3693228 c inspects : 382184 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=1476395008 c Current CPU time (ms) : 545.151 c starts : 148 c conflicts : 0 c decisions : 3600843 c propagations : 3718352 c inspects : 384612 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=1476395008 c Current CPU time (ms) : 547.609 c starts : 149 c conflicts : 0 c decisions : 3625173 c propagations : 3743476 c inspects : 387040 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=1476395008 c Current CPU time (ms) : 550.021 c starts : 150 c conflicts : 0 c decisions : 3649503 c propagations : 3768600 c inspects : 389466 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=1476395008 c Current CPU time (ms) : 552.361 c starts : 151 c conflicts : 0 c decisions : 3673833 c propagations : 3793724 c inspects : 391894 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=1476395008 c Current CPU time (ms) : 554.823 c starts : 152 c conflicts : 0 c decisions : 3698163 c propagations : 3818848 c inspects : 394323 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=1476395008 c Current CPU time (ms) : 557.213 c starts : 153 c conflicts : 0 c decisions : 3722493 c propagations : 3843972 c inspects : 396752 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=1476395008 c Current CPU time (ms) : 559.68 c starts : 154 c conflicts : 0 c decisions : 3746823 c propagations : 3869096 c inspects : 399179 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=1476395008 c Current CPU time (ms) : 561.984 c starts : 155 c conflicts : 0 c decisions : 3771153 c propagations : 3894220 c inspects : 401607 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=1476395008 c Current CPU time (ms) : 564.4 c starts : 156 c conflicts : 0 c decisions : 3795483 c propagations : 3919344 c inspects : 404034 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=1476395008 c Current CPU time (ms) : 566.87 c starts : 157 c conflicts : 0 c decisions : 3819813 c propagations : 3944468 c inspects : 406459 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=1476395008 c Current CPU time (ms) : 569.274 c starts : 158 c conflicts : 0 c decisions : 3844143 c propagations : 3969592 c inspects : 408886 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=1476395008 c Current CPU time (ms) : 571.614 c starts : 159 c conflicts : 0 c decisions : 3868473 c propagations : 3994716 c inspects : 411315 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=1476395008 c Current CPU time (ms) : 573.987 c starts : 160 c conflicts : 0 c decisions : 3892803 c propagations : 4019840 c inspects : 413744 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=1476395008 c Current CPU time (ms) : 576.343 c starts : 161 c conflicts : 0 c decisions : 3917133 c propagations : 4044964 c inspects : 416173 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=1476395008 c Current CPU time (ms) : 578.72 c starts : 162 c conflicts : 0 c decisions : 3941463 c propagations : 4070088 c inspects : 418601 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=1476395008 c Current CPU time (ms) : 581.092 c starts : 163 c conflicts : 0 c decisions : 3965793 c propagations : 4095212 c inspects : 421032 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=1476395008 c Current CPU time (ms) : 583.444 c starts : 164 c conflicts : 0 c decisions : 3990123 c propagations : 4120336 c inspects : 423461 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=1476395008 c Current CPU time (ms) : 585.827 c starts : 165 c conflicts : 0 c decisions : 4014453 c propagations : 4145460 c inspects : 425889 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=1476395008 c Current CPU time (ms) : 588.226 c starts : 166 c conflicts : 0 c decisions : 4038783 c propagations : 4170584 c inspects : 428319 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=1476395008 c Current CPU time (ms) : 590.617 c starts : 167 c conflicts : 0 c decisions : 4063113 c propagations : 4195708 c inspects : 430749 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=1476395008 c Current CPU time (ms) : 593.03 c starts : 168 c conflicts : 0 c decisions : 4087443 c propagations : 4220832 c inspects : 433175 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=1476395008 c Current CPU time (ms) : 595.453 c starts : 169 c conflicts : 0 c decisions : 4111773 c propagations : 4245956 c inspects : 435603 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=1476395008 c Current CPU time (ms) : 597.918 c starts : 170 c conflicts : 0 c decisions : 4136103 c propagations : 4271080 c inspects : 438031 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=1476395008 c Current CPU time (ms) : 600.339 c starts : 171 c conflicts : 0 c decisions : 4160433 c propagations : 4296204 c inspects : 440458 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=1476395008 c Current CPU time (ms) : 602.671 c starts : 172 c conflicts : 0 c decisions : 4184763 c propagations : 4321328 c inspects : 442886 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=1476395008 c Current CPU time (ms) : 605.052 c starts : 173 c conflicts : 0 c decisions : 4209093 c propagations : 4346452 c inspects : 445312 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=1476395008 c Current CPU time (ms) : 607.399 c starts : 174 c conflicts : 0 c decisions : 4233423 c propagations : 4371576 c inspects : 447738 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=1476395008 c Current CPU time (ms) : 609.785 c starts : 175 c conflicts : 0 c decisions : 4257753 c propagations : 4396700 c inspects : 450166 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=1476395008 c Current CPU time (ms) : 612.136 c starts : 176 c conflicts : 0 c decisions : 4282083 c propagations : 4421824 c inspects : 452594 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=1476395008 c Current CPU time (ms) : 614.482 c starts : 177 c conflicts : 0 c decisions : 4306413 c propagations : 4446948 c inspects : 455023 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=1476395008 c Current CPU time (ms) : 616.855 c starts : 178 c conflicts : 0 c decisions : 4330743 c propagations : 4472072 c inspects : 457452 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=1476395008 c Current CPU time (ms) : 619.209 c starts : 179 c conflicts : 0 c decisions : 4355073 c propagations : 4497196 c inspects : 459881 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=1476395008 c Current CPU time (ms) : 621.596 c starts : 180 c conflicts : 0 c decisions : 4379403 c propagations : 4522320 c inspects : 462310 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=1476395008 c Current CPU time (ms) : 624.023 c starts : 181 c conflicts : 0 c decisions : 4403733 c propagations : 4547444 c inspects : 464736 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=1476395008 c Current CPU time (ms) : 626.447 c starts : 182 c conflicts : 0 c decisions : 4428063 c propagations : 4572568 c inspects : 467163 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=1476395008 c Current CPU time (ms) : 628.925 c starts : 183 c conflicts : 0 c decisions : 4452393 c propagations : 4597692 c inspects : 469591 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=1476395008 c Current CPU time (ms) : 631.346 c starts : 184 c conflicts : 0 c decisions : 4476723 c propagations : 4622816 c inspects : 472021 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=1476395008 c Current CPU time (ms) : 633.77 c starts : 185 c conflicts : 0 c decisions : 4501053 c propagations : 4647940 c inspects : 474450 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=1476395008 c Current CPU time (ms) : 636.241 c starts : 186 c conflicts : 0 c decisions : 4525383 c propagations : 4673064 c inspects : 476879 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=1476395008 c Current CPU time (ms) : 638.662 c starts : 187 c conflicts : 0 c decisions : 4549713 c propagations : 4698188 c inspects : 479309 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=1476395008 c Current CPU time (ms) : 641.132 c starts : 188 c conflicts : 0 c decisions : 4574043 c propagations : 4723312 c inspects : 481738 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=1476395008 c Current CPU time (ms) : 643.558 c starts : 189 c conflicts : 0 c decisions : 4598373 c propagations : 4748436 c inspects : 484166 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=1476395008 c Current CPU time (ms) : 645.874 c starts : 190 c conflicts : 0 c decisions : 4622703 c propagations : 4773560 c inspects : 486594 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=1476395008 c Current CPU time (ms) : 648.247 c starts : 191 c conflicts : 0 c decisions : 4647033 c propagations : 4798684 c inspects : 489018 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=1476395008 c Current CPU time (ms) : 650.647 c starts : 192 c conflicts : 0 c decisions : 4671363 c propagations : 4823808 c inspects : 491447 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=1476395008 c Current CPU time (ms) : 653.133 c starts : 193 c conflicts : 0 c decisions : 4695693 c propagations : 4848932 c inspects : 493876 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=1476395008 c Current CPU time (ms) : 655.542 c starts : 194 c conflicts : 0 c decisions : 4720023 c propagations : 4874056 c inspects : 496302 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=1476395008 c Current CPU time (ms) : 657.987 c starts : 195 c conflicts : 0 c decisions : 4744353 c propagations : 4899180 c inspects : 498734 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=1476395008 c Current CPU time (ms) : 660.49 c starts : 196 c conflicts : 0 c decisions : 4768683 c propagations : 4924304 c inspects : 501162 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=1476395008 c Current CPU time (ms) : 662.933 c starts : 197 c conflicts : 0 c decisions : 4793013 c propagations : 4949428 c inspects : 503589 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=1476395008 c Current CPU time (ms) : 665.291 c starts : 198 c conflicts : 0 c decisions : 4817343 c propagations : 4974552 c inspects : 506016 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=1476395008 c Current CPU time (ms) : 667.703 c starts : 199 c conflicts : 0 c decisions : 4841673 c propagations : 4999676 c inspects : 508442 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=1476395008 c Current CPU time (ms) : 670.142 c starts : 200 c conflicts : 0 c decisions : 4866003 c propagations : 5024800 c inspects : 510869 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=1476395008 c Current CPU time (ms) : 672.648 c starts : 201 c conflicts : 0 c decisions : 4890333 c propagations : 5049924 c inspects : 513299 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=1476395008 c Current CPU time (ms) : 675.005 c starts : 202 c conflicts : 0 c decisions : 4914663 c propagations : 5075048 c inspects : 515727 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=1476395008 c Current CPU time (ms) : 677.452 c starts : 203 c conflicts : 0 c decisions : 4938993 c propagations : 5100172 c inspects : 518150 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=1476395008 c Current CPU time (ms) : 679.953 c starts : 204 c conflicts : 0 c decisions : 4963323 c propagations : 5125296 c inspects : 520577 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=1476395008 c Current CPU time (ms) : 682.392 c starts : 205 c conflicts : 0 c decisions : 4987653 c propagations : 5150420 c inspects : 523006 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=1476395008 c Current CPU time (ms) : 684.899 c starts : 206 c conflicts : 0 c decisions : 5011983 c propagations : 5175544 c inspects : 525432 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=1476395008 c Current CPU time (ms) : 687.324 c starts : 207 c conflicts : 0 c decisions : 5036313 c propagations : 5200668 c inspects : 527862 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=1476395008 c Current CPU time (ms) : 689.734 c starts : 208 c conflicts : 0 c decisions : 5060643 c propagations : 5225792 c inspects : 530291 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=1476395008 c Current CPU time (ms) : 692.213 c starts : 209 c conflicts : 0 c decisions : 5084973 c propagations : 5250916 c inspects : 532718 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=1476395008 c Current CPU time (ms) : 694.633 c starts : 210 c conflicts : 0 c decisions : 5109303 c propagations : 5276040 c inspects : 535148 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=1476395008 c Current CPU time (ms) : 696.968 c starts : 211 c conflicts : 0 c decisions : 5133633 c propagations : 5301164 c inspects : 537577 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=1476395008 c Current CPU time (ms) : 699.443 c starts : 212 c conflicts : 0 c decisions : 5157963 c propagations : 5326288 c inspects : 540005 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=1476395008 c Current CPU time (ms) : 701.874 c starts : 213 c conflicts : 0 c decisions : 5182293 c propagations : 5351412 c inspects : 542434 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=1476395008 c Current CPU time (ms) : 704.348 c starts : 214 c conflicts : 0 c decisions : 5206623 c propagations : 5376536 c inspects : 544860 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=1476395008 c Current CPU time (ms) : 706.675 c starts : 215 c conflicts : 0 c decisions : 5230953 c propagations : 5401660 c inspects : 547288 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=1476395008 c Current CPU time (ms) : 709.008 c starts : 216 c conflicts : 0 c decisions : 5255283 c propagations : 5426784 c inspects : 549717 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=1476395008 c Current CPU time (ms) : 711.481 c starts : 217 c conflicts : 0 c decisions : 5279613 c propagations : 5451908 c inspects : 552145 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=1476395008 c Current CPU time (ms) : 713.899 c starts : 218 c conflicts : 0 c decisions : 5303943 c propagations : 5477032 c inspects : 554575 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=1476395008 c Current CPU time (ms) : 716.371 c starts : 219 c conflicts : 0 c decisions : 5328273 c propagations : 5502156 c inspects : 557005 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=1476395008 c Current CPU time (ms) : 718.696 c starts : 220 c conflicts : 0 c decisions : 5352603 c propagations : 5527280 c inspects : 559433 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=1476395008 c Current CPU time (ms) : 721.053 c starts : 221 c conflicts : 0 c decisions : 5376933 c propagations : 5552404 c inspects : 561863 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=1476395008 c Current CPU time (ms) : 723.525 c starts : 222 c conflicts : 0 c decisions : 5401263 c propagations : 5577528 c inspects : 564292 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=1476395008 c Current CPU time (ms) : 725.954 c starts : 223 c conflicts : 0 c decisions : 5425593 c propagations : 5602652 c inspects : 566718 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=1476395008 c Current CPU time (ms) : 728.296 c starts : 224 c conflicts : 0 c decisions : 5449923 c propagations : 5627776 c inspects : 569148 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=1476395008 c Current CPU time (ms) : 730.673 c starts : 225 c conflicts : 0 c decisions : 5474253 c propagations : 5652900 c inspects : 571578 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=1476395008 c Current CPU time (ms) : 733.021 c starts : 226 c conflicts : 0 c decisions : 5498583 c propagations : 5678024 c inspects : 574007 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=1476395008 c Current CPU time (ms) : 735.504 c starts : 227 c conflicts : 0 c decisions : 5522913 c propagations : 5703148 c inspects : 576436 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=1476395008 c Current CPU time (ms) : 737.872 c starts : 228 c conflicts : 0 c decisions : 5547243 c propagations : 5728272 c inspects : 578864 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=1476395008 c Current CPU time (ms) : 740.334 c starts : 229 c conflicts : 0 c decisions : 5571573 c propagations : 5753396 c inspects : 581294 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=1476395008 c Current CPU time (ms) : 742.802 c starts : 230 c conflicts : 0 c decisions : 5595903 c propagations : 5778520 c inspects : 583725 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=1476395008 c Current CPU time (ms) : 745.228 c starts : 231 c conflicts : 0 c decisions : 5620233 c propagations : 5803644 c inspects : 586156 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=1476395008 c Current CPU time (ms) : 747.613 c starts : 232 c conflicts : 0 c decisions : 5644563 c propagations : 5828768 c inspects : 588587 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=1476395008 c Current CPU time (ms) : 749.98 c starts : 233 c conflicts : 0 c decisions : 5668893 c propagations : 5853892 c inspects : 591015 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=1476395008 c Current CPU time (ms) : 752.404 c starts : 234 c conflicts : 0 c decisions : 5693223 c propagations : 5879016 c inspects : 593444 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=1476395008 c Current CPU time (ms) : 754.78 c starts : 235 c conflicts : 0 c decisions : 5717553 c propagations : 5904140 c inspects : 595871 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=1476395008 c Current CPU time (ms) : 757.118 c starts : 236 c conflicts : 0 c decisions : 5741883 c propagations : 5929264 c inspects : 598299 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=1476395008 c Current CPU time (ms) : 759.454 c starts : 237 c conflicts : 0 c decisions : 5766213 c propagations : 5954388 c inspects : 600728 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=1476395008 c Current CPU time (ms) : 761.828 c starts : 238 c conflicts : 0 c decisions : 5790543 c propagations : 5979512 c inspects : 603156 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=1476395008 c Current CPU time (ms) : 764.18 c starts : 239 c conflicts : 0 c decisions : 5814873 c propagations : 6004636 c inspects : 605586 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=1476395008 c Current CPU time (ms) : 766.559 c starts : 240 c conflicts : 0 c decisions : 5839203 c propagations : 6029760 c inspects : 608013 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=1476395008 c Current CPU time (ms) : 768.919 c starts : 241 c conflicts : 0 c decisions : 5863533 c propagations : 6054884 c inspects : 610439 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=1476395008 c Current CPU time (ms) : 771.267 c starts : 242 c conflicts : 0 c decisions : 5887863 c propagations : 6080008 c inspects : 612866 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=1476395008 c Current CPU time (ms) : 773.752 c starts : 243 c conflicts : 0 c decisions : 5912193 c propagations : 6105132 c inspects : 615291 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=1476395008 c Current CPU time (ms) : 776.179 c starts : 244 c conflicts : 0 c decisions : 5936523 c propagations : 6130256 c inspects : 617719 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=1476395008 c Current CPU time (ms) : 778.58 c starts : 245 c conflicts : 0 c decisions : 5960853 c propagations : 6155380 c inspects : 620148 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=1476395008 c Current CPU time (ms) : 780.944 c starts : 246 c conflicts : 0 c decisions : 5985183 c propagations : 6180504 c inspects : 622577 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=1476395008 c Current CPU time (ms) : 783.373 c starts : 247 c conflicts : 0 c decisions : 6009513 c propagations : 6205628 c inspects : 625003 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=1476395008 c Current CPU time (ms) : 785.847 c starts : 248 c conflicts : 0 c decisions : 6033843 c propagations : 6230752 c inspects : 627429 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=1476395008 c Current CPU time (ms) : 788.277 c starts : 249 c conflicts : 0 c decisions : 6058173 c propagations : 6255876 c inspects : 629856 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=1476395008 c Current CPU time (ms) : 790.702 c starts : 250 c conflicts : 0 c decisions : 6082503 c propagations : 6281000 c inspects : 632284 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=1476395008 c Current CPU time (ms) : 793.182 c starts : 251 c conflicts : 0 c decisions : 6106833 c propagations : 6306124 c inspects : 634711 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=1476395008 c Current CPU time (ms) : 795.542 c starts : 252 c conflicts : 0 c decisions : 6131163 c propagations : 6331248 c inspects : 637138 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=1476395008 c Current CPU time (ms) : 798.023 c starts : 253 c conflicts : 0 c decisions : 6155493 c propagations : 6356372 c inspects : 639569 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=1476395008 c Current CPU time (ms) : 800.441 c starts : 254 c conflicts : 0 c decisions : 6179823 c propagations : 6381496 c inspects : 641997 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=1476395008 c Current CPU time (ms) : 802.823 c starts : 255 c conflicts : 0 c decisions : 6204153 c propagations : 6406620 c inspects : 644426 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=1476395008 c Current CPU time (ms) : 806.08 c starts : 256 c conflicts : 0 c decisions : 6228483 c propagations : 6431744 c inspects : 646857 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=1476395008 c Current CPU time (ms) : 808.526 c starts : 257 c conflicts : 0 c decisions : 6252813 c propagations : 6456868 c inspects : 649284 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=1476395008 c Current CPU time (ms) : 811.021 c starts : 258 c conflicts : 0 c decisions : 6277143 c propagations : 6481992 c inspects : 651716 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=1476395008 c Current CPU time (ms) : 813.416 c starts : 259 c conflicts : 0 c decisions : 6301473 c propagations : 6507116 c inspects : 654144 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=1476395008 c Current CPU time (ms) : 815.796 c starts : 260 c conflicts : 0 c decisions : 6325803 c propagations : 6532240 c inspects : 656573 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=1476395008 c Current CPU time (ms) : 818.329 c starts : 261 c conflicts : 0 c decisions : 6350133 c propagations : 6557364 c inspects : 658999 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=1476395008 c Current CPU time (ms) : 820.791 c starts : 262 c conflicts : 0 c decisions : 6374463 c propagations : 6582488 c inspects : 661427 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=1476395008 c Current CPU time (ms) : 823.229 c starts : 263 c conflicts : 0 c decisions : 6398793 c propagations : 6607612 c inspects : 663857 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=1476395008 c Current CPU time (ms) : 825.738 c starts : 264 c conflicts : 0 c decisions : 6423123 c propagations : 6632736 c inspects : 666287 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=1476395008 c Current CPU time (ms) : 828.128 c starts : 265 c conflicts : 0 c decisions : 6447453 c propagations : 6657860 c inspects : 668719 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=1476395008 c Current CPU time (ms) : 830.656 c starts : 266 c conflicts : 0 c decisions : 6471783 c propagations : 6682984 c inspects : 671143 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=1476395008 c Current CPU time (ms) : 833.06 c starts : 267 c conflicts : 0 c decisions : 6496113 c propagations : 6708108 c inspects : 673569 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=1476395008 c Current CPU time (ms) : 835.497 c starts : 268 c conflicts : 0 c decisions : 6520443 c propagations : 6733232 c inspects : 675996 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=1476395008 c Current CPU time (ms) : 837.902 c starts : 269 c conflicts : 0 c decisions : 6544773 c propagations : 6758356 c inspects : 678420 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=1476395008 c Current CPU time (ms) : 840.365 c starts : 270 c conflicts : 0 c decisions : 6569103 c propagations : 6783480 c inspects : 680848 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=1476395008 c Current CPU time (ms) : 842.868 c starts : 271 c conflicts : 0 c decisions : 6593433 c propagations : 6808604 c inspects : 683277 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=1476395008 c Current CPU time (ms) : 845.225 c starts : 272 c conflicts : 0 c decisions : 6617763 c propagations : 6833728 c inspects : 685706 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=1476395008 c Current CPU time (ms) : 847.593 c starts : 273 c conflicts : 0 c decisions : 6642093 c propagations : 6858852 c inspects : 688135 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=1476395008 c Current CPU time (ms) : 849.995 c starts : 274 c conflicts : 0 c decisions : 6666423 c propagations : 6883976 c inspects : 690566 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=1476395008 c Current CPU time (ms) : 852.369 c starts : 275 c conflicts : 0 c decisions : 6690753 c propagations : 6909100 c inspects : 692995 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=1476395008 c Current CPU time (ms) : 854.775 c starts : 276 c conflicts : 0 c decisions : 6715083 c propagations : 6934224 c inspects : 695424 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=1476395008 c Current CPU time (ms) : 857.157 c starts : 277 c conflicts : 0 c decisions : 6739413 c propagations : 6959348 c inspects : 697852 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=1476395008 c Current CPU time (ms) : 859.602 c starts : 278 c conflicts : 0 c decisions : 6763743 c propagations : 6984472 c inspects : 700283 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=1476395008 c Current CPU time (ms) : 862.013 c starts : 279 c conflicts : 0 c decisions : 6788073 c propagations : 7009596 c inspects : 702710 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=1476395008 c Current CPU time (ms) : 864.381 c starts : 280 c conflicts : 0 c decisions : 6812403 c propagations : 7034720 c inspects : 705135 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=1476395008 c Current CPU time (ms) : 866.791 c starts : 281 c conflicts : 0 c decisions : 6836733 c propagations : 7059844 c inspects : 707562 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=1476395008 c Current CPU time (ms) : 869.166 c starts : 282 c conflicts : 0 c decisions : 6861063 c propagations : 7084968 c inspects : 709987 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=1476395008 c Current CPU time (ms) : 871.539 c starts : 283 c conflicts : 0 c decisions : 6885393 c propagations : 7110092 c inspects : 712415 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=1476395008 c Current CPU time (ms) : 874.032 c starts : 284 c conflicts : 0 c decisions : 6909723 c propagations : 7135216 c inspects : 714843 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=1476395008 c Current CPU time (ms) : 876.456 c starts : 285 c conflicts : 0 c decisions : 6934053 c propagations : 7160340 c inspects : 717272 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=1476395008 c Current CPU time (ms) : 878.819 c starts : 286 c conflicts : 0 c decisions : 6958383 c propagations : 7185464 c inspects : 719699 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=1476395008 c Current CPU time (ms) : 881.319 c starts : 287 c conflicts : 0 c decisions : 6982713 c propagations : 7210588 c inspects : 722129 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=1476395008 c Current CPU time (ms) : 883.76 c starts : 288 c conflicts : 0 c decisions : 7007043 c propagations : 7235712 c inspects : 724557 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=1476395008 c Current CPU time (ms) : 886.162 c starts : 289 c conflicts : 0 c decisions : 7031373 c propagations : 7260836 c inspects : 726985 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=1476395008 c Current CPU time (ms) : 888.641 c starts : 290 c conflicts : 0 c decisions : 7055703 c propagations : 7285960 c inspects : 729416 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=1476395008 c Current CPU time (ms) : 891.087 c starts : 291 c conflicts : 0 c decisions : 7080033 c propagations : 7311084 c inspects : 731842 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=1476395008 c Current CPU time (ms) : 893.586 c starts : 292 c conflicts : 0 c decisions : 7104363 c propagations : 7336208 c inspects : 734271 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=1476395008 c Current CPU time (ms) : 895.935 c starts : 293 c conflicts : 0 c decisions : 7128693 c propagations : 7361332 c inspects : 736699 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=1476395008 c Current CPU time (ms) : 898.336 c starts : 294 c conflicts : 0 c decisions : 7153023 c propagations : 7386456 c inspects : 739128 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=1476395008 c Current CPU time (ms) : 900.719 c starts : 295 c conflicts : 0 c decisions : 7177353 c propagations : 7411580 c inspects : 741557 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=1476395008 c Current CPU time (ms) : 903.084 c starts : 296 c conflicts : 0 c decisions : 7201683 c propagations : 7436704 c inspects : 743985 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=1476395008 c Current CPU time (ms) : 905.489 c starts : 297 c conflicts : 0 c decisions : 7226013 c propagations : 7461828 c inspects : 746414 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=1476395008 c Current CPU time (ms) : 907.862 c starts : 298 c conflicts : 0 c decisions : 7250343 c propagations : 7486952 c inspects : 748842 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=1476395008 c Current CPU time (ms) : 910.232 c starts : 299 c conflicts : 0 c decisions : 7274673 c propagations : 7512076 c inspects : 751272 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=1476395008 c Current CPU time (ms) : 912.731 c starts : 300 c conflicts : 0 c decisions : 7299003 c propagations : 7537200 c inspects : 753700 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=1476395008 c Current CPU time (ms) : 915.183 c starts : 301 c conflicts : 0 c decisions : 7323333 c propagations : 7562324 c inspects : 756126 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=1476395008 c Current CPU time (ms) : 917.696 c starts : 302 c conflicts : 0 c decisions : 7347663 c propagations : 7587448 c inspects : 758555 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=1476395008 c Current CPU time (ms) : 920.048 c starts : 303 c conflicts : 0 c decisions : 7371993 c propagations : 7612572 c inspects : 760984 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=1476395008 c Current CPU time (ms) : 922.412 c starts : 304 c conflicts : 0 c decisions : 7396323 c propagations : 7637696 c inspects : 763412 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=1476395008 c Current CPU time (ms) : 924.817 c starts : 305 c conflicts : 0 c decisions : 7420653 c propagations : 7662820 c inspects : 765842 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=1476395008 c Current CPU time (ms) : 927.248 c starts : 306 c conflicts : 0 c decisions : 7444983 c propagations : 7687944 c inspects : 768271 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=1476395008 c Current CPU time (ms) : 929.774 c starts : 307 c conflicts : 0 c decisions : 7469313 c propagations : 7713068 c inspects : 770701 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=1476395008 c Current CPU time (ms) : 932.221 c starts : 308 c conflicts : 0 c decisions : 7493643 c propagations : 7738192 c inspects : 773129 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=1476395008 c Current CPU time (ms) : 934.669 c starts : 309 c conflicts : 0 c decisions : 7517973 c propagations : 7763316 c inspects : 775556 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=1476395008 c Current CPU time (ms) : 937.084 c starts : 310 c conflicts : 0 c decisions : 7542303 c propagations : 7788440 c inspects : 777984 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=1476395008 c Current CPU time (ms) : 939.472 c starts : 311 c conflicts : 0 c decisions : 7566633 c propagations : 7813564 c inspects : 780413 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=1476395008 c Current CPU time (ms) : 941.845 c starts : 312 c conflicts : 0 c decisions : 7590963 c propagations : 7838688 c inspects : 782842 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=1476395008 c Current CPU time (ms) : 944.261 c starts : 313 c conflicts : 0 c decisions : 7615293 c propagations : 7863812 c inspects : 785270 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=1476395008 c Current CPU time (ms) : 946.633 c starts : 314 c conflicts : 0 c decisions : 7639623 c propagations : 7888936 c inspects : 787700 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=1476395008 c Current CPU time (ms) : 949.152 c starts : 315 c conflicts : 0 c decisions : 7663953 c propagations : 7914060 c inspects : 790129 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=1476395008 c Current CPU time (ms) : 951.613 c starts : 316 c conflicts : 0 c decisions : 7688283 c propagations : 7939184 c inspects : 792556 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=1476395008 c Current CPU time (ms) : 953.975 c starts : 317 c conflicts : 0 c decisions : 7712613 c propagations : 7964308 c inspects : 794983 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=1476395008 c Current CPU time (ms) : 956.388 c starts : 318 c conflicts : 0 c decisions : 7736943 c propagations : 7989432 c inspects : 797410 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=1476395008 c Current CPU time (ms) : 958.767 c starts : 319 c conflicts : 0 c decisions : 7761273 c propagations : 8014556 c inspects : 799839 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=1476395008 c Current CPU time (ms) : 961.285 c starts : 320 c conflicts : 0 c decisions : 7785603 c propagations : 8039680 c inspects : 802265 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=1476395008 c Current CPU time (ms) : 963.662 c starts : 321 c conflicts : 0 c decisions : 7809933 c propagations : 8064804 c inspects : 804694 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=1476395008 c Current CPU time (ms) : 966.019 c starts : 322 c conflicts : 0 c decisions : 7834263 c propagations : 8089928 c inspects : 807121 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=1476395008 c Current CPU time (ms) : 968.525 c starts : 323 c conflicts : 0 c decisions : 7858593 c propagations : 8115052 c inspects : 809552 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=1476395008 c Current CPU time (ms) : 970.983 c starts : 324 c conflicts : 0 c decisions : 7882923 c propagations : 8140176 c inspects : 811979 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=1476395008 c Current CPU time (ms) : 973.44 c starts : 325 c conflicts : 0 c decisions : 7907253 c propagations : 8165300 c inspects : 814406 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=1476395008 c Current CPU time (ms) : 975.949 c starts : 326 c conflicts : 0 c decisions : 7931583 c propagations : 8190424 c inspects : 816834 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=1476395008 c Current CPU time (ms) : 978.406 c starts : 327 c conflicts : 0 c decisions : 7955913 c propagations : 8215548 c inspects : 819264 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=1476395008 c Current CPU time (ms) : 980.914 c starts : 328 c conflicts : 0 c decisions : 7980243 c propagations : 8240672 c inspects : 821692 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=1476395008 c Current CPU time (ms) : 983.362 c starts : 329 c conflicts : 0 c decisions : 8004573 c propagations : 8265796 c inspects : 824120 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=1476395008 c Current CPU time (ms) : 985.816 c starts : 330 c conflicts : 0 c decisions : 8028903 c propagations : 8290920 c inspects : 826549 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=1476395008 c Current CPU time (ms) : 988.232 c starts : 331 c conflicts : 0 c decisions : 8053233 c propagations : 8316044 c inspects : 828978 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=1476395008 c Current CPU time (ms) : 990.611 c starts : 332 c conflicts : 0 c decisions : 8077563 c propagations : 8341168 c inspects : 831408 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=1476395008 c Current CPU time (ms) : 993.031 c starts : 333 c conflicts : 0 c decisions : 8101893 c propagations : 8366292 c inspects : 833835 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=1476395008 c Current CPU time (ms) : 995.4 c starts : 334 c conflicts : 0 c decisions : 8126223 c propagations : 8391416 c inspects : 836266 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=1476395008 c Current CPU time (ms) : 997.782 c starts : 335 c conflicts : 0 c decisions : 8150553 c propagations : 8416540 c inspects : 838696 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=1476395008 c Current CPU time (ms) : 1000.179 c starts : 336 c conflicts : 0 c decisions : 8174883 c propagations : 8441664 c inspects : 841123 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=1476395008 c Current CPU time (ms) : 1002.565 c starts : 337 c conflicts : 0 c decisions : 8199213 c propagations : 8466788 c inspects : 843553 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=1476395008 c Current CPU time (ms) : 1005.027 c starts : 338 c conflicts : 0 c decisions : 8223543 c propagations : 8491912 c inspects : 845980 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=1476395008 c Current CPU time (ms) : 1007.435 c starts : 339 c conflicts : 0 c decisions : 8247873 c propagations : 8517036 c inspects : 848407 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=1476395008 c Current CPU time (ms) : 1009.816 c starts : 340 c conflicts : 0 c decisions : 8272203 c propagations : 8542160 c inspects : 850835 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=1476395008 c Current CPU time (ms) : 1012.234 c starts : 341 c conflicts : 0 c decisions : 8296533 c propagations : 8567284 c inspects : 853262 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=1476395008 c Current CPU time (ms) : 1014.583 c starts : 342 c conflicts : 0 c decisions : 8320863 c propagations : 8592408 c inspects : 855689 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=1476395008 c Current CPU time (ms) : 1016.963 c starts : 343 c conflicts : 0 c decisions : 8345193 c propagations : 8617532 c inspects : 858119 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=1476395008 c Current CPU time (ms) : 1019.371 c starts : 344 c conflicts : 0 c decisions : 8369523 c propagations : 8642656 c inspects : 860549 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=1476395008 c Current CPU time (ms) : 1021.766 c starts : 345 c conflicts : 0 c decisions : 8393853 c propagations : 8667780 c inspects : 862975 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=1476395008 c Current CPU time (ms) : 1024.276 c starts : 346 c conflicts : 0 c decisions : 8418183 c propagations : 8692904 c inspects : 865404 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=1476395008 c Current CPU time (ms) : 1026.659 c starts : 347 c conflicts : 0 c decisions : 8442513 c propagations : 8718028 c inspects : 867833 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=1476395008 c Current CPU time (ms) : 1029.035 c starts : 348 c conflicts : 0 c decisions : 8466843 c propagations : 8743152 c inspects : 870260 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=1476395008 c Current CPU time (ms) : 1031.535 c starts : 349 c conflicts : 0 c decisions : 8491173 c propagations : 8768276 c inspects : 872687 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=1476395008 c Current CPU time (ms) : 1033.928 c starts : 350 c conflicts : 0 c decisions : 8515503 c propagations : 8793400 c inspects : 875114 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=1476395008 c Current CPU time (ms) : 1036.385 c starts : 351 c conflicts : 0 c decisions : 8539833 c propagations : 8818524 c inspects : 877542 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=1476395008 c Current CPU time (ms) : 1038.802 c starts : 352 c conflicts : 0 c decisions : 8564163 c propagations : 8843648 c inspects : 879968 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=1476395008 c Current CPU time (ms) : 1041.19 c starts : 353 c conflicts : 0 c decisions : 8588493 c propagations : 8868772 c inspects : 882397 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=1476395008 c Current CPU time (ms) : 1043.61 c starts : 354 c conflicts : 0 c decisions : 8612823 c propagations : 8893896 c inspects : 884827 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=1476395008 c Current CPU time (ms) : 1046.001 c starts : 355 c conflicts : 0 c decisions : 8637153 c propagations : 8919020 c inspects : 887256 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=1476395008 c Current CPU time (ms) : 1048.48 c starts : 356 c conflicts : 0 c decisions : 8661483 c propagations : 8944144 c inspects : 889683 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=1476395008 c Current CPU time (ms) : 1050.904 c starts : 357 c conflicts : 0 c decisions : 8685813 c propagations : 8969268 c inspects : 892112 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=1476395008 c Current CPU time (ms) : 1053.358 c starts : 358 c conflicts : 0 c decisions : 8710143 c propagations : 8994392 c inspects : 894539 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=1476395008 c Current CPU time (ms) : 1055.866 c starts : 359 c conflicts : 0 c decisions : 8734473 c propagations : 9019516 c inspects : 896967 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=1476395008 c Current CPU time (ms) : 1058.26 c starts : 360 c conflicts : 0 c decisions : 8758803 c propagations : 9044640 c inspects : 899395 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=1476395008 c Current CPU time (ms) : 1060.65 c starts : 361 c conflicts : 0 c decisions : 8783133 c propagations : 9069764 c inspects : 901825 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=1476395008 c Current CPU time (ms) : 1063.153 c starts : 362 c conflicts : 0 c decisions : 8807463 c propagations : 9094888 c inspects : 904253 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=1476395008 c Current CPU time (ms) : 1065.616 c starts : 363 c conflicts : 0 c decisions : 8831793 c propagations : 9120012 c inspects : 906682 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=1476395008 c Current CPU time (ms) : 1068.075 c starts : 364 c conflicts : 0 c decisions : 8856123 c propagations : 9145136 c inspects : 909109 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=1476395008 c Current CPU time (ms) : 1070.593 c starts : 365 c conflicts : 0 c decisions : 8880453 c propagations : 9170260 c inspects : 911539 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=1476395008 c Current CPU time (ms) : 1073.037 c starts : 366 c conflicts : 0 c decisions : 8904783 c propagations : 9195384 c inspects : 913965 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=1476395008 c Current CPU time (ms) : 1075.461 c starts : 367 c conflicts : 0 c decisions : 8929113 c propagations : 9220508 c inspects : 916394 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=1476395008 c Current CPU time (ms) : 1077.921 c starts : 368 c conflicts : 0 c decisions : 8953443 c propagations : 9245632 c inspects : 918824 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=1476395008 c Current CPU time (ms) : 1080.389 c starts : 369 c conflicts : 0 c decisions : 8977773 c propagations : 9270756 c inspects : 921253 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=1476395008 c Current CPU time (ms) : 1082.799 c starts : 370 c conflicts : 0 c decisions : 9002103 c propagations : 9295880 c inspects : 923681 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=1476395008 c Current CPU time (ms) : 1085.265 c starts : 371 c conflicts : 0 c decisions : 9026433 c propagations : 9321004 c inspects : 926112 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=1476395008 c Current CPU time (ms) : 1087.777 c starts : 372 c conflicts : 0 c decisions : 9050763 c propagations : 9346128 c inspects : 928541 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=1476395008 c Current CPU time (ms) : 1090.242 c starts : 373 c conflicts : 0 c decisions : 9075093 c propagations : 9371252 c inspects : 930966 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=1476395008 c Current CPU time (ms) : 1092.702 c starts : 374 c conflicts : 0 c decisions : 9099423 c propagations : 9396376 c inspects : 933396 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=1476395008 c Current CPU time (ms) : 1095.218 c starts : 375 c conflicts : 0 c decisions : 9123753 c propagations : 9421500 c inspects : 935826 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=1476395008 c Current CPU time (ms) : 1097.671 c starts : 376 c conflicts : 0 c decisions : 9148083 c propagations : 9446624 c inspects : 938253 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=1476395008 c Current CPU time (ms) : 1100.14 c starts : 377 c conflicts : 0 c decisions : 9172413 c propagations : 9471748 c inspects : 940682 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=1476395008 c Current CPU time (ms) : 1102.55 c starts : 378 c conflicts : 0 c decisions : 9196743 c propagations : 9496872 c inspects : 943108 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=1476395008 c Current CPU time (ms) : 1104.943 c starts : 379 c conflicts : 0 c decisions : 9221073 c propagations : 9521996 c inspects : 945537 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=1476395008 c Current CPU time (ms) : 1107.361 c starts : 380 c conflicts : 0 c decisions : 9245403 c propagations : 9547120 c inspects : 947965 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=1476395008 c Current CPU time (ms) : 1109.762 c starts : 381 c conflicts : 0 c decisions : 9269733 c propagations : 9572244 c inspects : 950393 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=1476395008 c Current CPU time (ms) : 1112.138 c starts : 382 c conflicts : 0 c decisions : 9294063 c propagations : 9597368 c inspects : 952819 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=1476395008 c Current CPU time (ms) : 1114.652 c starts : 383 c conflicts : 0 c decisions : 9318393 c propagations : 9622492 c inspects : 955249 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=1476395008 c Current CPU time (ms) : 1117.113 c starts : 384 c conflicts : 0 c decisions : 9342723 c propagations : 9647616 c inspects : 957677 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=1476395008 c Current CPU time (ms) : 1119.683 c starts : 385 c conflicts : 0 c decisions : 9367053 c propagations : 9672740 c inspects : 960106 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=1476395008 c Current CPU time (ms) : 1122.171 c starts : 386 c conflicts : 0 c decisions : 9391383 c propagations : 9697864 c inspects : 962533 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=1476395008 c Current CPU time (ms) : 1124.618 c starts : 387 c conflicts : 0 c decisions : 9415713 c propagations : 9722988 c inspects : 964962 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=1476395008 c Current CPU time (ms) : 1127.074 c starts : 388 c conflicts : 0 c decisions : 9440043 c propagations : 9748112 c inspects : 967388 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=1476395008 c Current CPU time (ms) : 1129.425 c starts : 389 c conflicts : 0 c decisions : 9464373 c propagations : 9773236 c inspects : 969816 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=1476395008 c Current CPU time (ms) : 1131.894 c starts : 390 c conflicts : 0 c decisions : 9488703 c propagations : 9798360 c inspects : 972244 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=1476395008 c Current CPU time (ms) : 1134.247 c starts : 391 c conflicts : 0 c decisions : 9513033 c propagations : 9823484 c inspects : 974673 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=1476395008 c Current CPU time (ms) : 1136.696 c starts : 392 c conflicts : 0 c decisions : 9537363 c propagations : 9848608 c inspects : 977101 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=1476395008 c Current CPU time (ms) : 1139.206 c starts : 393 c conflicts : 0 c decisions : 9561693 c propagations : 9873732 c inspects : 979527 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=1476395008 c Current CPU time (ms) : 1141.586 c starts : 394 c conflicts : 0 c decisions : 9586023 c propagations : 9898856 c inspects : 981954 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=1476395008 c Current CPU time (ms) : 1144.058 c starts : 395 c conflicts : 0 c decisions : 9610353 c propagations : 9923980 c inspects : 984378 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=1476395008 c Current CPU time (ms) : 1146.494 c starts : 396 c conflicts : 0 c decisions : 9634683 c propagations : 9949104 c inspects : 986806 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=1476395008 c Current CPU time (ms) : 1148.98 c starts : 397 c conflicts : 0 c decisions : 9659013 c propagations : 9974228 c inspects : 989235 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=1476395008 c Current CPU time (ms) : 1151.522 c starts : 398 c conflicts : 0 c decisions : 9683343 c propagations : 9999352 c inspects : 991662 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=1476395008 c Current CPU time (ms) : 1153.991 c starts : 399 c conflicts : 0 c decisions : 9707673 c propagations : 10024476 c inspects : 994089 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=1476395008 c Current CPU time (ms) : 1156.46 c starts : 400 c conflicts : 0 c decisions : 9732003 c propagations : 10049600 c inspects : 996519 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=1476395008 c Current CPU time (ms) : 1158.989 c starts : 401 c conflicts : 0 c decisions : 9756333 c propagations : 10074724 c inspects : 998945 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=1476395008 c Current CPU time (ms) : 1161.368 c starts : 402 c conflicts : 0 c decisions : 9780663 c propagations : 10099848 c inspects : 1001373 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=1476395008 c Current CPU time (ms) : 1163.798 c starts : 403 c conflicts : 0 c decisions : 9804993 c propagations : 10124972 c inspects : 1003801 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=1476395008 c Current CPU time (ms) : 1166.263 c starts : 404 c conflicts : 0 c decisions : 9829323 c propagations : 10150096 c inspects : 1006227 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=1476395008 c Current CPU time (ms) : 1168.734 c starts : 405 c conflicts : 0 c decisions : 9853653 c propagations : 10175220 c inspects : 1008658 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=1476395008 c Current CPU time (ms) : 1171.242 c starts : 406 c conflicts : 0 c decisions : 9877983 c propagations : 10200344 c inspects : 1011084 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=1476395008 c Current CPU time (ms) : 1173.713 c starts : 407 c conflicts : 0 c decisions : 9902313 c propagations : 10225468 c inspects : 1013511 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=1476395008 c Current CPU time (ms) : 1176.185 c starts : 408 c conflicts : 0 c decisions : 9926643 c propagations : 10250592 c inspects : 1015941 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=1476395008 c Current CPU time (ms) : 1178.607 c starts : 409 c conflicts : 0 c decisions : 9950973 c propagations : 10275716 c inspects : 1018368 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=1476395008 c Current CPU time (ms) : 1180.984 c starts : 410 c conflicts : 0 c decisions : 9975303 c propagations : 10300840 c inspects : 1020797 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=1476395008 c Current CPU time (ms) : 1183.414 c starts : 411 c conflicts : 0 c decisions : 9999633 c propagations : 10325964 c inspects : 1023224 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=1476395008 c Current CPU time (ms) : 1185.814 c starts : 412 c conflicts : 0 c decisions : 10023963 c propagations : 10351088 c inspects : 1025652 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=1476395008 c Current CPU time (ms) : 1188.206 c starts : 413 c conflicts : 0 c decisions : 10048293 c propagations : 10376212 c inspects : 1028081 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=1476395008 c Current CPU time (ms) : 1190.621 c starts : 414 c conflicts : 0 c decisions : 10072623 c propagations : 10401336 c inspects : 1030508 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=1476395008 c Current CPU time (ms) : 1193.096 c starts : 415 c conflicts : 0 c decisions : 10096953 c propagations : 10426460 c inspects : 1032937 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=1476395008 c Current CPU time (ms) : 1195.619 c starts : 416 c conflicts : 0 c decisions : 10121283 c propagations : 10451584 c inspects : 1035362 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=1476395008 c Current CPU time (ms) : 1197.993 c starts : 417 c conflicts : 0 c decisions : 10145613 c propagations : 10476708 c inspects : 1037792 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=1476395008 c Current CPU time (ms) : 1200.463 c starts : 418 c conflicts : 0 c decisions : 10169943 c propagations : 10501832 c inspects : 1040220 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=1476395008 c Current CPU time (ms) : 1202.992 c starts : 419 c conflicts : 0 c decisions : 10194273 c propagations : 10526956 c inspects : 1042649 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=1476395008 c Current CPU time (ms) : 1205.371 c starts : 420 c conflicts : 0 c decisions : 10218603 c propagations : 10552080 c inspects : 1045077 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=1476395008 c Current CPU time (ms) : 1207.849 c starts : 421 c conflicts : 0 c decisions : 10242933 c propagations : 10577204 c inspects : 1047505 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=1476395008 c Current CPU time (ms) : 1210.365 c starts : 422 c conflicts : 0 c decisions : 10267263 c propagations : 10602328 c inspects : 1049932 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=1476395008 c Current CPU time (ms) : 1212.838 c starts : 423 c conflicts : 0 c decisions : 10291593 c propagations : 10627452 c inspects : 1052361 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=1476395008 c Current CPU time (ms) : 1215.36 c starts : 424 c conflicts : 0 c decisions : 10315923 c propagations : 10652576 c inspects : 1054788 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=1476395008 c Current CPU time (ms) : 1217.835 c starts : 425 c conflicts : 0 c decisions : 10340253 c propagations : 10677700 c inspects : 1057218 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=1476395008 c Current CPU time (ms) : 1220.289 c starts : 426 c conflicts : 0 c decisions : 10364583 c propagations : 10702824 c inspects : 1059645 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=1476395008 c Current CPU time (ms) : 1222.818 c starts : 427 c conflicts : 0 c decisions : 10388913 c propagations : 10727948 c inspects : 1062074 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=1476395008 c Current CPU time (ms) : 1225.203 c starts : 428 c conflicts : 0 c decisions : 10413243 c propagations : 10753072 c inspects : 1064502 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=1476395008 c Current CPU time (ms) : 1227.643 c starts : 429 c conflicts : 0 c decisions : 10437573 c propagations : 10778196 c inspects : 1066933 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=1476395008 c Current CPU time (ms) : 1230.026 c starts : 430 c conflicts : 0 c decisions : 10461903 c propagations : 10803320 c inspects : 1069361 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=1476395008 c Current CPU time (ms) : 1232.505 c starts : 431 c conflicts : 0 c decisions : 10486233 c propagations : 10828444 c inspects : 1071790 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=1476395008 c Current CPU time (ms) : 1235.028 c starts : 432 c conflicts : 0 c decisions : 10510563 c propagations : 10853568 c inspects : 1074221 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=1476395008 c Current CPU time (ms) : 1237.417 c starts : 433 c conflicts : 0 c decisions : 10534893 c propagations : 10878692 c inspects : 1076650 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=1476395008 c Current CPU time (ms) : 1239.801 c starts : 434 c conflicts : 0 c decisions : 10559223 c propagations : 10903816 c inspects : 1079078 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=1476395008 c Current CPU time (ms) : 1242.332 c starts : 435 c conflicts : 0 c decisions : 10583553 c propagations : 10928940 c inspects : 1081509 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=1476395008 c Current CPU time (ms) : 1244.802 c starts : 436 c conflicts : 0 c decisions : 10607883 c propagations : 10954064 c inspects : 1083937 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=1476395008 c Current CPU time (ms) : 1247.24 c starts : 437 c conflicts : 0 c decisions : 10632213 c propagations : 10979188 c inspects : 1086366 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=1476395008 c Current CPU time (ms) : 1249.623 c starts : 438 c conflicts : 0 c decisions : 10656543 c propagations : 11004312 c inspects : 1088794 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=1476395008 c Current CPU time (ms) : 1251.994 c starts : 439 c conflicts : 0 c decisions : 10680873 c propagations : 11029436 c inspects : 1091223 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=1476395008 c Current CPU time (ms) : 1254.399 c starts : 440 c conflicts : 0 c decisions : 10705203 c propagations : 11054560 c inspects : 1093651 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=1476395008 c Current CPU time (ms) : 1256.765 c starts : 441 c conflicts : 0 c decisions : 10729533 c propagations : 11079684 c inspects : 1096078 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=1476395008 c Current CPU time (ms) : 1259.265 c starts : 442 c conflicts : 0 c decisions : 10753863 c propagations : 11104808 c inspects : 1098507 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=1476395008 c Current CPU time (ms) : 1261.718 c starts : 443 c conflicts : 0 c decisions : 10778193 c propagations : 11129932 c inspects : 1100933 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=1476395008 c Current CPU time (ms) : 1264.074 c starts : 444 c conflicts : 0 c decisions : 10802523 c propagations : 11155056 c inspects : 1103362 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=1476395008 c Current CPU time (ms) : 1266.579 c starts : 445 c conflicts : 0 c decisions : 10826853 c propagations : 11180180 c inspects : 1105791 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=1476395008 c Current CPU time (ms) : 1269.025 c starts : 446 c conflicts : 0 c decisions : 10851183 c propagations : 11205304 c inspects : 1108219 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=1476395008 c Current CPU time (ms) : 1271.468 c starts : 447 c conflicts : 0 c decisions : 10875513 c propagations : 11230428 c inspects : 1110646 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=1476395008 c Current CPU time (ms) : 1273.969 c starts : 448 c conflicts : 0 c decisions : 10899843 c propagations : 11255552 c inspects : 1113076 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=1476395008 c Current CPU time (ms) : 1276.426 c starts : 449 c conflicts : 0 c decisions : 10924173 c propagations : 11280676 c inspects : 1115504 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=1476395008 c Current CPU time (ms) : 1278.926 c starts : 450 c conflicts : 0 c decisions : 10948503 c propagations : 11305800 c inspects : 1117932 c learned literals : 0 c learned binary clauses : 0 c learned ternary clauses : 0 c learned clauses : 0 c root simplifications : 450 #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.86 0.92 2/54 5674 Raw data (stat): 5674 (runsolver) R 5673 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544274526 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.93 0.86 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18027 0 1 0 818 42 0 0 25 0 10 0 544274526 860413952 20839 4294967295 134512640 134569956 3221224400 3221214728 1131176513 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 210062 20839 13073 16 0 210046 0 vsize: 840248 [startup+20.0013 s] Raw data (loadavg): 0.94 0.87 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 1699 42 0 0 25 0 10 0 544274526 859627520 21248 4294967295 134512640 134569956 3221224400 3221214820 1080204031 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 21248 13073 16 0 209854 0 vsize: 839480 [startup+30.0019 s] Raw data (loadavg): 0.95 0.87 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 2573 42 0 0 25 0 10 0 544274526 859627520 21820 4294967295 134512640 134569956 3221224400 3221214832 1131313866 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209870 21820 13073 16 0 209854 0 vsize: 839480 [startup+40.0027 s] Raw data (loadavg): 0.95 0.87 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 3481 43 0 0 25 0 10 0 544274526 859627520 22093 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22093 13073 16 0 209854 0 vsize: 839480 [startup+50.0085 s] Raw data (loadavg): 0.96 0.88 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 4396 44 0 0 25 0 10 0 544274526 859627520 22250 4294967295 134512640 134569956 3221224400 3221214820 1080203551 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22250 13073 16 0 209854 0 vsize: 839480 [startup+60.0092 s] Raw data (loadavg): 0.97 0.88 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 5309 44 0 0 24 0 10 0 544274526 859627520 22380 4294967295 134512640 134569956 3221224400 3221214280 1077558376 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22380 13073 16 0 209854 0 vsize: 839480 [startup+70.0109 s] Raw data (loadavg): 0.97 0.89 0.92 2/63 5683 Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18028 0 1 0 6237 44 0 0 25 0 10 0 544274526 859627520 22604 4294967295 134512640 134569956 3221224400 3221213520 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22604 13073 16 0 209854 0 vsize: 839480 [startup+80.0117 s] Raw data (loadavg): 0.98 0.89 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 7170 45 0 0 24 0 10 0 544274526 859627520 22712 4294967295 134512640 134569956 3221224400 3221214296 1080019622 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22712 13073 16 0 209854 0 vsize: 839480 [startup+90.0127 s] Raw data (loadavg): 0.98 0.89 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 8104 45 0 0 25 0 10 0 544274526 859627520 22805 4294967295 134512640 134569956 3221224400 3221214280 1077558376 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22805 13073 16 0 209854 0 vsize: 839480 [startup+100.014 s] Raw data (loadavg): 0.98 0.89 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 9039 46 0 0 25 0 10 0 544274526 859627520 22893 4294967295 134512640 134569956 3221224400 3221214776 1131176395 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22893 13073 16 0 209854 0 vsize: 839480 [startup+110.014 s] Raw data (loadavg): 0.98 0.90 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 9976 46 0 0 25 0 10 0 544274526 859627520 22975 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 22975 13073 16 0 209854 0 vsize: 839480 [startup+120.014 s] Raw data (loadavg): 0.99 0.90 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 10912 47 0 0 25 0 10 0 544274526 859627520 23053 4294967295 134512640 134569956 3221224400 3221214828 1080204163 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 23053 13073 16 0 209854 0 vsize: 839480 [startup+130.014 s] Raw data (loadavg): 0.99 0.90 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 11844 47 0 0 24 0 10 0 544274526 859627520 23130 4294967295 134512640 134569956 3221224400 3221214296 1080019608 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 23130 13073 16 0 209854 0 vsize: 839480 [startup+140.015 s] Raw data (loadavg): 0.99 0.91 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 12780 47 0 0 25 0 10 0 544274526 859627520 23202 4294967295 134512640 134569956 3221224400 3221214820 1080203551 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 23202 13073 16 0 209854 0 vsize: 839480 [startup+150.015 s] Raw data (loadavg): 0.99 0.91 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 13716 48 0 0 25 0 10 0 544274526 859627520 23269 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 23269 13073 16 0 209854 0 vsize: 839480 [startup+160.014 s] Raw data (loadavg): 0.99 0.91 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 14642 48 0 0 25 0 10 0 544274526 859627520 23335 4294967295 134512640 134569956 3221224400 3221214296 1080019608 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 23335 13073 16 0 209854 0 vsize: 839480 [startup+170.015 s] Raw data (loadavg): 0.99 0.91 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 15534 50 0 0 25 0 10 0 544274526 859627520 23421 4294967295 134512640 134569956 3221224400 3221214296 1080019608 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 23421 13073 16 0 209854 0 vsize: 839480 [startup+180.015 s] Raw data (loadavg): 0.99 0.92 0.92 2/63 5683 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 16398 50 0 0 25 0 10 0 544274526 859627520 24044 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209870 24044 13073 16 0 209854 0 vsize: 839480 [startup+190.016 s] Raw data (loadavg): 0.99 0.92 0.92 2/64 5684 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18058 0 1 0 17267 53 0 0 25 0 11 0 544274526 860155904 30055 4294967295 134512640 134569956 3221224400 3221214776 1131394326 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 30055 13073 16 0 209983 0 vsize: 839996 [startup+200.016 s] Raw data (loadavg): 0.99 0.92 0.92 2/64 5687 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 18209 54 0 0 25 0 11 0 544274526 860155904 30072 4294967295 134512640 134569956 3221224400 3221214648 1131353685 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 30072 13073 16 0 209983 0 vsize: 839996 [startup+210.017 s] Raw data (loadavg): 1.07 0.94 0.93 2/64 5691 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 19141 54 0 0 25 0 11 0 544274526 860155904 30072 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 30072 13073 16 0 209983 0 vsize: 839996 [startup+220.017 s] Raw data (loadavg): 1.06 0.94 0.93 2/64 5695 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 20065 55 0 0 25 0 11 0 544274526 860155904 30248 4294967295 134512640 134569956 3221224400 3221214808 1131397952 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 30248 13073 16 0 209983 0 vsize: 839996 [startup+230.018 s] Raw data (loadavg): 1.05 0.94 0.93 2/64 5699 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 20999 56 0 0 25 0 11 0 544274526 860155904 30383 4294967295 134512640 134569956 3221224400 3221214736 1131357348 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 30383 13073 16 0 209983 0 vsize: 839996 [startup+240.019 s] Raw data (loadavg): 1.12 0.96 0.93 2/64 5703 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 21954 56 0 0 25 0 11 0 544274526 860155904 31678 4294967295 134512640 134569956 3221224400 3221214736 1131357787 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 31678 13073 16 0 209983 0 vsize: 839996 [startup+250.019 s] Raw data (loadavg): 1.10 0.96 0.93 2/64 5708 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 22925 57 0 0 25 0 11 0 544274526 860155904 31678 4294967295 134512640 134569956 3221224400 3221214648 1131352402 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 31678 13073 16 0 209983 0 vsize: 839996 [startup+260.019 s] Raw data (loadavg): 1.08 0.96 0.93 2/64 5712 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 23879 57 0 0 25 0 11 0 544274526 860155904 31679 4294967295 134512640 134569956 3221224400 3221214736 1131357442 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 31679 13073 16 0 209983 0 vsize: 839996 [startup+270.032 s] Raw data (loadavg): 1.07 0.96 0.93 2/64 5716 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 24819 58 1 0 25 0 11 0 544274526 860155904 32075 4294967295 134512640 134569956 3221224400 3221214648 1131352442 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 32075 13073 16 0 209983 0 vsize: 839996 [startup+280.032 s] Raw data (loadavg): 1.06 0.96 0.93 2/64 5720 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 25793 59 1 0 25 0 11 0 544274526 860155904 33914 4294967295 134512640 134569956 3221224400 3221214648 1131353717 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 33914 13073 16 0 209983 0 vsize: 839996 [startup+290.033 s] Raw data (loadavg): 1.05 0.96 0.93 2/64 5725 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 26759 59 1 0 25 0 11 0 544274526 860155904 33914 4294967295 134512640 134569956 3221224400 3221214736 1131357341 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 33914 13073 16 0 209983 0 vsize: 839996 [startup+300.042 s] Raw data (loadavg): 1.04 0.97 0.93 2/64 5729 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 27713 60 1 0 25 0 11 0 544274526 860155904 33914 4294967295 134512640 134569956 3221224400 3221214808 1131394127 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 33914 13073 16 0 209983 0 vsize: 839996 [startup+310.041 s] Raw data (loadavg): 1.04 0.97 0.93 2/64 5733 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 28658 61 1 0 25 0 11 0 544274526 860155904 34079 4294967295 134512640 134569956 3221224400 3221214808 1131393350 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 34079 13073 16 0 209983 0 vsize: 839996 [startup+320.041 s] Raw data (loadavg): 1.03 0.97 0.93 2/64 5737 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 29600 61 1 0 25 0 11 0 544274526 860155904 34225 4294967295 134512640 134569956 3221224400 3221214648 1131353705 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 34225 13073 16 0 209983 0 vsize: 839996 [startup+330.147 s] Raw data (loadavg): 1.02 0.97 0.93 2/64 5742 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 30555 62 2 0 25 0 11 0 544274526 860155904 34354 4294967295 134512640 134569956 3221224400 3221214880 1131347785 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 34354 13073 16 0 209983 0 vsize: 839996 [startup+340.147 s] Raw data (loadavg): 1.02 0.97 0.93 2/64 5746 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 31496 62 2 0 25 0 11 0 544274526 860155904 34641 4294967295 134512640 134569956 3221224400 3221214648 1131352439 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 34641 13073 16 0 209983 0 vsize: 839996 [startup+350.147 s] Raw data (loadavg): 1.02 0.97 0.93 2/64 5750 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 32432 63 2 0 25 0 11 0 544274526 860155904 37918 4294967295 134512640 134569956 3221224400 3221214736 1131357381 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 37918 13073 16 0 209983 0 vsize: 839996 [startup+360.147 s] Raw data (loadavg): 1.01 0.97 0.93 2/64 5754 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 33375 63 2 0 25 0 11 0 544274526 860155904 38050 4294967295 134512640 134569956 3221224400 3221214804 1131423212 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 38050 13073 16 0 209983 0 vsize: 839996 [startup+370.179 s] Raw data (loadavg): 1.01 0.97 0.93 2/64 5758 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 34323 64 2 0 25 0 11 0 544274526 860155904 38179 4294967295 134512640 134569956 3221224400 3221214736 1131357752 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 38179 13073 16 0 209983 0 vsize: 839996 [startup+380.179 s] Raw data (loadavg): 1.01 0.97 0.93 2/64 5762 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 35267 64 2 0 25 0 11 0 544274526 860155904 38418 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 38418 13073 16 0 209983 0 vsize: 839996 [startup+390.179 s] Raw data (loadavg): 1.01 0.97 0.93 2/64 5767 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 36213 64 3 0 25 0 11 0 544274526 860155904 38547 4294967295 134512640 134569956 3221224400 3221215032 1131407238 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 38547 13073 16 0 209983 0 vsize: 839996 [startup+400.18 s] Raw data (loadavg): 1.01 0.97 0.93 2/64 5771 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 37160 65 3 1 25 0 11 0 544274526 860155904 38709 4294967295 134512640 134569956 3221224400 3221214648 1131352341 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 38709 13073 16 0 209983 0 vsize: 839996 [startup+410.18 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5775 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 38107 65 3 1 25 0 11 0 544274526 860155904 38872 4294967295 134512640 134569956 3221224400 3221214808 1131395207 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 38872 13073 16 0 209983 0 vsize: 839996 [startup+420.18 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5779 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 39055 66 3 1 25 0 11 0 544274526 860155904 39001 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 39001 13073 16 0 209983 0 vsize: 839996 [startup+430.18 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5783 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 39995 66 3 1 25 0 11 0 544274526 860155904 39130 4294967295 134512640 134569956 3221224400 3221214736 1131357450 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 39130 13073 16 0 209983 0 vsize: 839996 [startup+440.181 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5788 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 40933 67 4 1 25 0 11 0 544274526 860155904 39259 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 39259 13073 16 0 209983 0 vsize: 839996 [startup+450.181 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5792 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 41871 67 4 1 25 0 11 0 544274526 860155904 39421 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 39421 13073 16 0 209983 0 vsize: 839996 [startup+460.181 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5796 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 42814 67 4 1 25 0 11 0 544274526 860155904 39798 4294967295 134512640 134569956 3221224400 3221214648 1131352372 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 39798 13073 16 0 209983 0 vsize: 839996 [startup+470.182 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5800 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 43761 68 4 1 25 0 11 0 544274526 860155904 39928 4294967295 134512640 134569956 3221224400 3221214736 1131357350 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 39928 13073 16 0 209983 0 vsize: 839996 [startup+480.182 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5804 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 44709 69 4 1 25 0 11 0 544274526 860155904 40057 4294967295 134512640 134569956 3221224400 3221214648 1131352639 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 40057 13073 16 0 209983 0 vsize: 839996 [startup+490.182 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5808 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 45654 69 5 1 25 0 11 0 544274526 860155904 40192 4294967295 134512640 134569956 3221224400 3221214736 1131357350 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 40192 13073 16 0 209983 0 vsize: 839996 [startup+500.182 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5812 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 46579 70 5 1 25 0 11 0 544274526 860155904 46647 4294967295 134512640 134569956 3221224400 3221214648 1131352379 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 46647 13073 16 0 209983 0 vsize: 839996 [startup+510.183 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5817 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 47518 70 5 1 24 0 11 0 544274526 860155904 46776 4294967295 134512640 134569956 3221224400 3221214736 1131357370 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 46776 13073 16 0 209983 0 vsize: 839996 [startup+520.183 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5821 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 48458 71 5 2 25 0 11 0 544274526 860155904 46905 4294967295 134512640 134569956 3221224400 3221214808 1131394326 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 46905 13073 16 0 209983 0 vsize: 839996 [startup+530.182 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5825 Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 49400 71 5 2 25 0 11 0 544274526 860155904 47143 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 47143 13073 16 0 209983 0 vsize: 839996 [startup+540.184 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5829 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 50344 72 5 2 25 0 11 0 544274526 860155904 47381 4294967295 134512640 134569956 3221224400 3221214736 1131357773 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 47381 13073 16 0 209983 0 vsize: 839996 [startup+550.185 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5833 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 51294 72 5 2 25 0 11 0 544274526 860155904 47510 4294967295 134512640 134569956 3221224400 3221214736 1131357685 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 47510 13073 16 0 209983 0 vsize: 839996 [startup+560.184 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5837 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 52240 73 6 2 25 0 11 0 544274526 860155904 47640 4294967295 134512640 134569956 3221224400 3221214648 1131352653 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 47640 13073 16 0 209983 0 vsize: 839996 [startup+570.186 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5842 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 53185 74 6 2 25 0 11 0 544274526 860155904 47770 4294967295 134512640 134569956 3221224400 3221214736 1131357801 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 47770 13073 16 0 209983 0 vsize: 839996 [startup+580.186 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5846 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 54130 74 6 2 25 0 11 0 544274526 860155904 47899 4294967295 134512640 134569956 3221224400 3221214648 1131352289 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 47899 13073 16 0 209983 0 vsize: 839996 [startup+590.187 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5850 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 55072 75 6 2 25 0 11 0 544274526 860155904 48061 4294967295 134512640 134569956 3221224400 3221214808 1131395136 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48061 13073 16 0 209983 0 vsize: 839996 [startup+600.187 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5854 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 56020 75 6 2 25 0 11 0 544274526 860155904 48256 4294967295 134512640 134569956 3221224400 3221214648 1131353636 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48256 13073 16 0 209983 0 vsize: 839996 [startup+610.187 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5858 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 56966 75 7 2 25 0 11 0 544274526 860155904 48385 4294967295 134512640 134569956 3221224400 3221214648 1131352579 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48385 13073 16 0 209983 0 vsize: 839996 [startup+620.188 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5863 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 57914 76 7 2 25 0 11 0 544274526 860155904 48514 4294967295 134512640 134569956 3221224400 3221214736 1131357832 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48514 13073 16 0 209983 0 vsize: 839996 [startup+630.188 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5867 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 58860 77 7 2 25 0 11 0 544274526 860155904 48644 4294967295 134512640 134569956 3221224400 3221214976 1131410945 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48644 13073 16 0 209983 0 vsize: 839996 [startup+640.19 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5871 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 59805 77 7 2 25 0 11 0 544274526 860155904 48805 4294967295 134512640 134569956 3221224400 3221214808 1131393226 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48805 13073 16 0 209983 0 vsize: 839996 [startup+650.19 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5875 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 60751 78 7 2 25 0 11 0 544274526 860155904 48934 4294967295 134512640 134569956 3221224400 3221214808 1131397843 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 48934 13073 16 0 209983 0 vsize: 839996 [startup+660.19 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5879 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 61687 78 8 2 20 0 11 0 544274526 860155904 49128 4294967295 134512640 134569956 3221224400 3221214804 1131185452 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 49128 13073 16 0 209983 0 vsize: 839996 [startup+670.191 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5883 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 62622 80 8 3 24 0 11 0 544274526 860155904 49257 4294967295 134512640 134569956 3221224400 3221214760 1131185520 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 49257 13073 16 0 209983 0 vsize: 839996 [startup+680.191 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5887 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 63563 80 8 3 25 0 11 0 544274526 860155904 49454 4294967295 134512640 134569956 3221224400 3221214808 1131393226 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 49454 13073 16 0 209983 0 vsize: 839996 [startup+690.193 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5891 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 64503 81 8 3 25 0 11 0 544274526 860155904 49945 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 49945 13073 16 0 209983 0 vsize: 839996 [startup+700.196 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5896 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 65449 81 8 3 25 0 11 0 544274526 860155904 50074 4294967295 134512640 134569956 3221224400 3221214832 1131382771 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50074 13073 16 0 209983 0 vsize: 839996 [startup+710.196 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5900 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 66394 82 8 3 25 0 11 0 544274526 860155904 50236 4294967295 134512640 134569956 3221224400 3221214688 1131329914 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50236 13073 16 0 209983 0 vsize: 839996 [startup+720.201 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5904 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 67341 82 9 3 25 0 11 0 544274526 860155904 50365 4294967295 134512640 134569956 3221224400 3221214736 1131357798 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50365 13073 16 0 209983 0 vsize: 839996 [startup+730.201 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5908 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 68287 83 9 3 25 0 11 0 544274526 860155904 50494 4294967295 134512640 134569956 3221224400 3221214648 1131353232 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50494 13073 16 0 209983 0 vsize: 839996 [startup+740.201 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5912 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 69233 84 9 3 24 0 11 0 544274526 860155904 50624 4294967295 134512640 134569956 3221224400 3221214732 1131352256 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50624 13073 16 0 209983 0 vsize: 839996 [startup+750.207 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5916 Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 70183 84 9 4 25 0 11 0 544274526 860155904 50753 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50753 13073 16 0 209983 0 vsize: 839996 [startup+760.207 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5921 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 71132 85 9 4 25 0 11 0 544274526 860155904 50894 4294967295 134512640 134569956 3221224400 3221214832 1131382808 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 50894 13073 16 0 209983 0 vsize: 839996 [startup+770.207 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5925 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 72074 85 9 4 24 0 11 0 544274526 860155904 51055 4294967295 134512640 134569956 3221224400 3221214760 1131185475 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 51055 13073 16 0 209983 0 vsize: 839996 [startup+780.206 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5929 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 73025 86 10 4 25 0 11 0 544274526 860155904 51153 4294967295 134512640 134569956 3221224400 3221214648 1131353659 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 51153 13073 16 0 209983 0 vsize: 839996 [startup+790.208 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5933 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 73970 86 10 4 25 0 11 0 544274526 860155904 51314 4294967295 134512640 134569956 3221224400 3221214648 1131352631 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 51314 13073 16 0 209983 0 vsize: 839996 [startup+800.208 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5937 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 74917 86 10 4 25 0 11 0 544274526 860155904 51443 4294967295 134512640 134569956 3221224400 3221214736 1131357442 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 51443 13073 16 0 209983 0 vsize: 839996 [startup+810.208 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5941 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 75820 87 10 4 25 0 11 0 544274526 860155904 64158 4294967295 134512640 134569956 3221224400 3221214736 1131357337 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 64158 13073 16 0 209983 0 vsize: 839996 [startup+820.209 s] Raw data (loadavg): 1.00 0.97 0.93 2/64 5945 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 76752 87 10 4 25 0 11 0 544274526 860155904 64288 4294967295 134512640 134569956 3221224400 3221214648 1131353404 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 64288 13073 16 0 209983 0 vsize: 839996 [startup+830.209 s] Raw data (loadavg): 1.08 0.99 0.94 2/64 5949 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 77685 88 10 5 25 0 11 0 544274526 860155904 64417 4294967295 134512640 134569956 3221224400 3221214760 1131185472 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 64417 13073 16 0 209983 0 vsize: 839996 [startup+840.21 s] Raw data (loadavg): 1.07 0.99 0.94 2/64 5953 Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 78622 89 10 5 25 0 11 0 544274526 860155904 64832 4294967295 134512640 134569956 3221224400 3221213352 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 64832 13073 16 0 209983 0 vsize: 839996 [startup+850.21 s] Raw data (loadavg): 1.06 0.99 0.94 2/64 5957 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 79566 89 10 5 25 0 11 0 544274526 860155904 65109 4294967295 134512640 134569956 3221224400 3221214648 1131352381 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65109 13073 16 0 209983 0 vsize: 839996 [startup+860.216 s] Raw data (loadavg): 1.05 0.99 0.94 2/64 5961 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 80511 89 11 5 25 0 11 0 544274526 860155904 65238 4294967295 134512640 134569956 3221224400 3221214044 1077094240 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65238 13073 16 0 209983 0 vsize: 839996 [startup+870.221 s] Raw data (loadavg): 1.04 0.99 0.94 2/64 5966 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 81455 90 11 5 25 0 11 0 544274526 860155904 65367 4294967295 134512640 134569956 3221224400 3221214808 1131393219 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65367 13073 16 0 209983 0 vsize: 839996 [startup+880.222 s] Raw data (loadavg): 1.03 0.99 0.94 2/64 5970 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 82399 90 11 5 25 0 11 0 544274526 860155904 65530 4294967295 134512640 134569956 3221224400 3221214648 1131352601 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65530 13073 16 0 209983 0 vsize: 839996 [startup+890.223 s] Raw data (loadavg): 1.03 0.99 0.94 2/64 5974 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 83345 91 11 5 25 0 11 0 544274526 860155904 65660 4294967295 134512640 134569956 3221224400 3221214648 1131352422 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65660 13073 16 0 209983 0 vsize: 839996 [startup+900.223 s] Raw data (loadavg): 1.02 0.99 0.94 2/64 5978 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 84290 91 11 5 25 0 11 0 544274526 860155904 65789 4294967295 134512640 134569956 3221224400 3221214760 1131185475 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65789 13073 16 0 209983 0 vsize: 839996 [startup+910.223 s] Raw data (loadavg): 1.02 0.99 0.94 2/64 5982 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 85236 92 11 5 25 0 11 0 544274526 860155904 65918 4294967295 134512640 134569956 3221224400 3221214736 1131357804 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 65918 13073 16 0 209983 0 vsize: 839996 [startup+920.224 s] Raw data (loadavg): 1.02 0.99 0.94 2/64 5986 Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 86182 92 11 5 25 0 11 0 544274526 860155904 66048 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66048 13073 16 0 209983 0 vsize: 839996 [startup+930.26 s] Raw data (loadavg): 1.01 0.99 0.94 2/64 5990 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 87134 93 11 5 25 0 11 0 544274526 860155904 66177 4294967295 134512640 134569956 3221224400 3221214736 1131357348 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66177 13073 16 0 209983 0 vsize: 839996 [startup+940.261 s] Raw data (loadavg): 1.01 0.99 0.94 2/64 5995 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 88075 94 11 6 25 0 11 0 544274526 860155904 66306 4294967295 134512640 134569956 3221224400 3221214808 1131394312 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66306 13073 16 0 209983 0 vsize: 839996 [startup+950.261 s] Raw data (loadavg): 1.01 0.99 0.94 2/64 5999 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 89016 94 12 6 25 0 11 0 544274526 860155904 66434 4294967295 134512640 134569956 3221224400 3221214808 1131395529 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66434 13073 16 0 209983 0 vsize: 839996 [startup+960.261 s] Raw data (loadavg): 1.01 0.99 0.94 2/64 6003 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 89956 94 12 6 25 0 11 0 544274526 860155904 66597 4294967295 134512640 134569956 3221224400 3221214808 1131393266 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66597 13073 16 0 209983 0 vsize: 839996 [startup+970.262 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6007 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 90898 95 12 6 25 0 11 0 544274526 860155904 66858 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66858 13073 16 0 209983 0 vsize: 839996 [startup+980.262 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6011 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 91847 96 12 6 25 0 11 0 544274526 860155904 66987 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 66987 13073 16 0 209983 0 vsize: 839996 [startup+990.263 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6015 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 92790 97 12 6 25 0 11 0 544274526 860155904 67117 4294967295 134512640 134569956 3221224400 3221214808 1131393226 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 67117 13073 16 0 209983 0 vsize: 839996 [startup+1000.26 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6019 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 93735 97 13 7 25 0 11 0 544274526 860155904 67246 4294967295 134512640 134569956 3221224400 3221214736 1131357341 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 67246 13073 16 0 209983 0 vsize: 839996 [startup+1010.26 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6023 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 94680 98 13 7 25 0 11 0 544274526 860155904 67374 4294967295 134512640 134569956 3221224400 3221214648 1131353363 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 67374 13073 16 0 209983 0 vsize: 839996 [startup+1020.26 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6028 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 95625 98 13 7 25 0 11 0 544274526 860155904 67503 4294967295 134512640 134569956 3221224400 3221214952 1131415243 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 67503 13073 16 0 209983 0 vsize: 839996 [startup+1030.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6032 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 96568 99 13 7 25 0 11 0 544274526 860155904 67666 4294967295 134512640 134569956 3221224400 3221214808 1131393007 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 67666 13073 16 0 209983 0 vsize: 839996 [startup+1040.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6036 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 97511 99 13 7 24 0 11 0 544274526 860155904 67794 4294967295 134512640 134569956 3221224400 3221214648 1131353659 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 67794 13073 16 0 209983 0 vsize: 839996 [startup+1050.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6040 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 98460 99 13 7 25 0 11 0 544274526 860155904 67923 4294967295 134512640 134569956 3221224400 3221214736 1131357438 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 67923 13073 16 0 209983 0 vsize: 839996 [startup+1060.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6044 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 99404 100 14 7 24 0 11 0 544274526 860155904 68052 4294967295 134512640 134569956 3221224400 3221214648 1131352617 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68052 13073 16 0 209983 0 vsize: 839996 [startup+1070.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6048 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 100348 101 14 7 25 0 11 0 544274526 860155904 68183 4294967295 134512640 134569956 3221224400 3221214736 1131357381 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68183 13073 16 0 209983 0 vsize: 839996 [startup+1080.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6052 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 101292 101 14 7 24 0 11 0 544274526 860155904 68311 4294967295 134512640 134569956 3221224400 3221214736 1131357716 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68311 13073 16 0 209983 0 vsize: 839996 [startup+1090.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6056 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 102241 102 14 7 25 0 11 0 544274526 860155904 68441 4294967295 134512640 134569956 3221224400 3221214648 1131352494 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68441 13073 16 0 209983 0 vsize: 839996 [startup+1100.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6060 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 103184 103 14 7 25 0 11 0 544274526 860155904 68570 4294967295 134512640 134569956 3221224400 3221214736 1131357728 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68570 13073 16 0 209983 0 vsize: 839996 [startup+1110.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6064 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 104129 103 14 7 25 0 11 0 544274526 860155904 68700 4294967295 134512640 134569956 3221224400 3221214736 1131357676 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68700 13073 16 0 209983 0 vsize: 839996 [startup+1120.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6068 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 105068 104 14 7 24 0 11 0 544274526 860155904 68929 4294967295 134512640 134569956 3221224400 3221214648 1131353644 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 68929 13073 16 0 209983 0 vsize: 839996 [startup+1130.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6073 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 106028 105 15 7 25 0 11 0 544274526 860155904 69804 4294967295 134512640 134569956 3221224400 3221214648 1131353287 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 69804 13073 16 0 209983 0 vsize: 839996 [startup+1140.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6077 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 106980 105 15 7 25 0 11 0 544274526 860155904 69804 4294967295 134512640 134569956 3221224400 3221214648 1131352381 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 69804 13073 16 0 209983 0 vsize: 839996 [startup+1150.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6081 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 107918 106 15 7 25 0 11 0 544274526 860155904 69804 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 69804 13073 16 0 209983 0 vsize: 839996 [startup+1160.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6085 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 108864 106 15 7 25 0 11 0 544274526 860155904 70367 4294967295 134512640 134569956 3221224400 3221214992 1131389937 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 70367 13073 16 0 209983 0 vsize: 839996 [startup+1170.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6089 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 109807 107 15 7 25 0 11 0 544274526 860155904 70528 4294967295 134512640 134569956 3221224400 3221214648 1131352355 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 70528 13073 16 0 209983 0 vsize: 839996 [startup+1180.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6093 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 110751 107 16 7 25 0 11 0 544274526 860155904 70657 4294967295 134512640 134569956 3221224400 3221214808 1131394312 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 70657 13073 16 0 209983 0 vsize: 839996 [startup+1190.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6097 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 111696 108 16 8 25 0 11 0 544274526 860155904 70787 4294967295 134512640 134569956 3221224400 3221214760 1131185475 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 70787 13073 16 0 209983 0 vsize: 839996 [startup+1200.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6101 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 112645 108 16 8 25 0 11 0 544274526 860155904 70916 4294967295 134512640 134569956 3221224400 3221214648 1131352631 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 70916 13073 16 0 209983 0 vsize: 839996 [startup+1210.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6105 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 113588 109 16 8 25 0 11 0 544274526 860155904 71044 4294967295 134512640 134569956 3221224400 3221214808 1131394326 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 71044 13073 16 0 209983 0 vsize: 839996 [startup+1220.27 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6109 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 114531 109 16 8 25 0 11 0 544274526 860155904 71173 4294967295 134512640 134569956 3221224400 3221214736 1131357804 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 71173 13073 16 0 209983 0 vsize: 839996 [startup+1230.28 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6113 Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 115475 110 16 8 25 0 11 0 544274526 860155904 71303 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 71303 13073 16 0 209983 0 vsize: 839996 [startup+1240.28 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6117 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 116424 110 16 8 25 0 11 0 544274526 860155904 71432 4294967295 134512640 134569956 3221224400 3221214808 1131394326 0 4 3 23756 0 0 0 17 1 0 0 Raw data (statm): 209999 71432 13073 16 0 209983 0 vsize: 839996 [startup+1250.28 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6121 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 117367 111 16 8 25 0 11 0 544274526 860155904 71561 4294967295 134512640 134569956 3221224400 3221214916 1130885120 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 71561 13073 16 0 209983 0 vsize: 839996 [startup+1260.28 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6126 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 118309 111 17 8 25 0 11 0 544274526 860155904 71691 4294967295 134512640 134569956 3221224400 3221214648 1131352488 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 71691 13073 16 0 209983 0 vsize: 839996 [startup+1270.28 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6130 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 119251 111 17 8 24 0 11 0 544274526 860155904 71852 4294967295 134512640 134569956 3221224400 3221214648 1131352280 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 71852 13073 16 0 209983 0 vsize: 839996 [startup+1280.28 s] Raw data (loadavg): 1.00 0.99 0.94 2/64 6134 Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 120199 112 17 8 25 0 11 0 544274526 860155904 71949 4294967295 134512640 134569956 3221224400 3221214688 1131330281 0 4 3 23756 0 0 0 17 0 0 0 Raw data (statm): 209999 71949 13073 16 0 209983 0 vsize: 839996 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1280.42 s] Raw data (loadavg): 1.00 0.99 0.94 1/54 6135 Raw data (stat): 5674 (java) Z 5673 27565 27564 0 -1 1036 18059 52196 1 0 120199 112 7478 131 25 0 1 0 544274526 0 0 4294967295 0 0 0 0 0 0 4 3 23756 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 143 Real time (s): 1280.42 CPU time (s): 1279.22 CPU user time (s): 1276.78 CPU system time (s): 2.44163 CPU usage (%): 99.9063 Max. virtual memory (Kb): 840248 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####