n=2 (0.0s): 
n=3 (0.0s): 
n=4 (0.0s): 
n=5 (0.0s): k=2,w>=4:UNSAT
n=6 (0.0s): k=2,w>=5:UNSAT
n=7 (0.0s): k=2,w>=6:UNSAT; k=3,w>=6:UNSAT
n=8 (0.0s): k=2,w>=6:UNSAT; k=3,w>=7:UNSAT
n=9 (0.0s): k=2,w>=7:UNSAT; k=3,w>=8:UNSAT; k=4,w>=8:UNSAT
n=10 (0.0s): k=2,w>=8:UNSAT; k=3,w>=9:UNSAT; k=4,w>=9:UNSAT
n=11 (0.0s): k=2,w>=8:UNSAT; k=3,w>=10:UNSAT; k=4,w>=10:UNSAT; k=5,w>=10:UNSAT
n=12 (0.0s): k=2,w>=9:UNSAT; k=3,w>=10:UNSAT; k=4,w>=11:UNSAT; k=5,w>=11:UNSAT
n=13 (0.0s): k=2,w>=10:UNSAT; k=3,w>=11:UNSAT; k=4,w>=12:UNSAT; k=5,w>=12:UNSAT; k=6,w>=12:UNSAT
n=14 (0.1s): k=2,w>=10:UNSAT; k=3,w>=12:UNSAT; k=4,w>=13:UNSAT; k=5,w>=13:UNSAT; k=6,w>=13:UNSAT
n=15 (0.2s): k=2,w>=11:UNSAT; k=3,w>=13:UNSAT; k=4,w>=14:UNSAT; k=5,w>=14:UNSAT; k=6,w>=14:UNSAT; k=7,w>=14:UNSAT
n=16 (0.7s): k=2,w>=12:UNSAT; k=3,w>=14:UNSAT; k=4,w>=14:UNSAT; k=5,w>=15:UNSAT; k=6,w>=15:UNSAT; k=7,w>=15:UNSAT
n=17 (1.6s): k=2,w>=12:UNSAT; k=3,w>=14:UNSAT; k=4,w>=15:UNSAT; k=5,w>=16:UNSAT; k=6,w>=16:UNSAT; k=7,w>=16:UNSAT; k=8,w>=16:UNSAT
n=18 (1.7s): k=2,w>=13:UNSAT; k=3,w>=15:UNSAT; k=4,w>=16:UNSAT; k=5,w>=17:UNSAT; k=6,w>=17:UNSAT; k=7,w>=17:UNSAT; k=8,w>=17:UNSAT
n=19 (3.8s): k=2,w>=14:UNSAT; k=3,w>=16:UNSAT; k=4,w>=17:UNSAT; k=5,w>=18:UNSAT; k=6,w>=18:UNSAT; k=7,w>=18:UNSAT; k=8,w>=18:UNSAT; k=9,w>=18:UNSAT
n=20 (31.3s): k=2,w>=14:UNSAT; k=3,w>=17:UNSAT; k=4,w>=18:UNSAT; k=5,w>=18:UNSAT; k=6,w>=19:UNSAT; k=7,w>=19:UNSAT; k=8,w>=19:UNSAT; k=9,w>=19:UNSAT
