N window heuristic helper

window_size_0_cnf(x)
window_size_1_cnf(x)
window_size_2_cnf(x)
window_size_3_cnf(x)
window_size_4_cnf(x)
window_size_5_cnf(x)
window_size_with_full_1_window_cnf(a, b, c, aux)
window_size_with_full_2_window_cnf(a, b, c, aux)
window_size_with_full_3_window_cnf(a, b, c, aux)
window_size_with_full_4_window_cnf(a, b, c, aux)