Optimizations On Lemma 5 C_5 + 2e > C^d_* Yes C_5 + 2e > C^+2_* No C_5 + 3e > C^+2_* No C_5 + 4e > C^+2_* Yes C_6 + 2e > C^d_* No C_6 + 3e > C^d_* No C_6 + 4e > C^d_* Yes C_6 + 4e > C^+2_* Yes C_7 + 2e > C^d_* No C_7 + 3e > C^d_* Yes C_7 + 3e > C^+2_* Yes C_8 + 2e > C^d_* No C_8 + 3e > C^d_* No C_8 + 4e > C^d_* No C_8 + 5e > C^d_* Yes C_8 + 5e > C^+2_* Yes Lemma 9 P_1 + P_3 + 2e >= C^d_* No P_1 + P_5 + 3e >= C^d_* No P_1 + P_7 + 4e >= C^d_* Yes P_1 + P_6 + 4e >= C^d_* Yes P_1 + P_5 + 4e >= C^d_* Yes P_1 + P_4 + 4e >= C^d_* Yes P_1 + P_3 + 4e >= C^d_* Yes P_1 + P_2 + 4e >= C^d_* Yes P_1 + P_1 + 4e >= C^d_* Yes P_1 + P_* + 4e >= C^d_* OK P_1 + P_7 + 4e > C^d_* No P_1 + P_9 + 5e > C^d_* Yes P_1 + P_8 + 5e > C^d_* Yes P_1 + P_7 + 5e > C^d_* Yes P_1 + P_6 + 5e > C^d_* Yes P_1 + P_5 + 5e > C^d_* Yes P_1 + P_4 + 5e > C^d_* Yes P_1 + P_3 + 5e > C^d_* Yes P_1 + P_2 + 5e > C^d_* Yes P_1 + P_1 + 5e > C^d_* Yes P_1 + P_* + 5e > C^d_* OK P_2 + P_3 + 2e >= C^d_* No P_2 + P_5 + 3e >= C^d_* No P_2 + P_7 + 4e >= C^d_* No P_2 + P_9 + 5e >= C^d_* Yes P_2 + P_8 + 5e >= C^d_* Yes P_2 + P_7 + 5e >= C^d_* Yes P_2 + P_6 + 5e >= C^d_* Yes P_2 + P_5 + 5e >= C^d_* Yes P_2 + P_4 + 5e >= C^d_* Yes P_2 + P_3 + 5e >= C^d_* Yes P_2 + P_2 + 5e >= C^d_* Yes P_2 + P_1 + 5e >= C^d_* Yes P_2 + P_* + 5e >= C^d_* OK P_2 + P_9 + 5e > C^d_* Yes P_2 + P_8 + 5e > C^d_* No P_2 + P_8 + 6e > C^d_* Yes P_2 + P_7 + 6e > C^d_* Yes P_2 + P_6 + 6e > C^d_* Yes P_2 + P_5 + 6e > C^d_* Yes P_2 + P_4 + 6e > C^d_* Yes P_2 + P_3 + 6e > C^d_* Yes P_2 + P_2 + 6e > C^d_* Yes P_2 + P_1 + 6e > C^d_* Yes P_2 + P_* + 6e > C^d_* OK P_3 + P_3 + 2e >= C^d_* No P_3 + P_5 + 3e >= C^d_* No P_3 + P_7 + 4e >= C^d_* No P_3 + P_9 + 5e >= C^d_* No P_3 + P_11 + 6e >= C^d_* Yes P_3 + P_10 + 6e >= C^d_* Yes P_3 + P_9 + 6e >= C^d_* Yes P_3 + P_8 + 6e >= C^d_* Yes P_3 + P_7 + 6e >= C^d_* Yes P_3 + P_6 + 6e >= C^d_* Yes P_3 + P_5 + 6e >= C^d_* Yes P_3 + P_4 + 6e >= C^d_* Yes P_3 + P_3 + 6e >= C^d_* Yes P_3 + P_2 + 6e >= C^d_* Yes P_3 + P_1 + 6e >= C^d_* Yes P_3 + P_* + 6e >= C^d_* OK P_3 + P_11 + 6e > C^d_* Yes P_3 + P_10 + 6e > C^d_* Yes P_3 + P_9 + 6e > C^d_* Yes P_3 + P_8 + 6e > C^d_* Yes P_3 + P_7 + 6e > C^d_* Yes P_3 + P_6 + 6e > C^d_* Yes P_3 + P_5 + 6e > C^d_* Yes P_3 + P_4 + 6e > C^d_* Yes P_3 + P_3 + 6e > C^d_* Yes P_3 + P_2 + 6e > C^d_* Yes P_3 + P_1 + 6e > C^d_* Yes P_3 + P_* + 6e > C^d_* OK P_4 + P_3 + 2e >= C^d_* No P_4 + P_5 + 3e >= C^d_* No P_4 + P_7 + 4e >= C^d_* No P_4 + P_9 + 5e >= C^d_* No P_4 + P_11 + 6e >= C^d_* Yes P_4 + P_10 + 6e >= C^d_* Yes P_4 + P_9 + 6e >= C^d_* Yes P_4 + P_8 + 6e >= C^d_* Yes P_4 + P_7 + 6e >= C^d_* Yes P_4 + P_6 + 6e >= C^d_* Yes P_4 + P_5 + 6e >= C^d_* Yes P_4 + P_4 + 6e >= C^d_* Yes P_4 + P_3 + 6e >= C^d_* Yes P_4 + P_2 + 6e >= C^d_* Yes P_4 + P_1 + 6e >= C^d_* Yes P_4 + P_* + 6e >= C^d_* OK P_4 + P_11 + 6e > C^d_* Yes P_4 + P_10 + 6e > C^d_* Yes P_4 + P_9 + 6e > C^d_* Yes P_4 + P_8 + 6e > C^d_* Yes P_4 + P_7 + 6e > C^d_* Yes P_4 + P_6 + 6e > C^d_* Yes P_4 + P_5 + 6e > C^d_* Yes P_4 + P_4 + 6e > C^d_* No P_4 + P_4 + 7e > C^d_* Yes P_4 + P_3 + 7e > C^d_* Yes P_4 + P_2 + 7e > C^d_* Yes P_4 + P_1 + 7e > C^d_* Yes P_4 + P_* + 7e > C^d_* OK P_5 + P_3 + 2e >= C^d_* No P_5 + P_5 + 3e >= C^d_* No P_5 + P_7 + 4e >= C^d_* No P_5 + P_9 + 5e >= C^d_* No P_5 + P_11 + 6e >= C^d_* No P_5 + P_13 + 7e >= C^d_* Yes P_5 + P_12 + 7e >= C^d_* Yes P_5 + P_11 + 7e >= C^d_* Yes P_5 + P_10 + 7e >= C^d_* Yes P_5 + P_9 + 7e >= C^d_* Yes P_5 + P_8 + 7e >= C^d_* Yes P_5 + P_7 + 7e >= C^d_* Yes P_5 + P_6 + 7e >= C^d_* Yes P_5 + P_5 + 7e >= C^d_* Yes P_5 + P_4 + 7e >= C^d_* Yes P_5 + P_3 + 7e >= C^d_* Yes P_5 + P_2 + 7e >= C^d_* Yes P_5 + P_1 + 7e >= C^d_* Yes P_5 + P_* + 7e >= C^d_* OK P_5 + P_13 + 7e > C^d_* Yes P_5 + P_12 + 7e > C^d_* Yes P_5 + P_11 + 7e > C^d_* Yes P_5 + P_10 + 7e > C^d_* Yes P_5 + P_9 + 7e > C^d_* Yes P_5 + P_8 + 7e > C^d_* Yes P_5 + P_7 + 7e > C^d_* Yes P_5 + P_6 + 7e > C^d_* Yes P_5 + P_5 + 7e > C^d_* Yes P_5 + P_4 + 7e > C^d_* Yes P_5 + P_3 + 7e > C^d_* Yes P_5 + P_2 + 7e > C^d_* Yes P_5 + P_1 + 7e > C^d_* Yes P_5 + P_* + 7e > C^d_* OK Lemma 10 C_4 + C_3 + 8e > C_* + C_* No C_4 + C_3 + 9e > C_* + C_* Yes C_4 + C_4 + 8e > C_* + C_* No C_4 + C_4 + 9e > C_* + C_* Yes C_4 + C_4 + 9e > C^d_* + C_* No C_4 + C_4 + 10e > C^d_* + C_* No C_4 + C_4 + 11e > C^d_* + C_* Yes C_5 + C_3 + 9e > C^d_* + C_* No C_5 + C_3 + 10e > C^d_* + C_* Yes C_5 + C_4 + 9e > C^d_* + C_* No C_5 + C_4 + 10e > C^d_* + C_* Yes C_5 + C_5 + 9e > C^d_* + C_* No C_5 + C_5 + 10e > C^d_* + C_* No C_5 + C_5 + 11e > C^d_* + C_* Yes C_6 + C_3 + 9e > C^d_* + C_* No C_6 + C_3 + 10e > C^d_* + C_* No C_6 + C_3 + 11e > C^d_* + C_* Yes C_6 + C_4 + 9e > C^d_* + C_* No C_6 + C_4 + 10e > C^d_* + C_* No C_6 + C_4 + 11e > C^d_* + C_* No C_6 + C_4 + 12e > C^d_* + C_* No C_6 + C_4 + 13e > C^d_* + C_* Yes C_6 + C_5 + 9e > C^d_* + C_* No C_6 + C_5 + 10e > C^d_* + C_* No C_6 + C_5 + 11e > C^d_* + C_* Yes C_6 + C_6 + 9e > C^d_* + C_* No C_6 + C_6 + 10e > C^d_* + C_* No C_6 + C_6 + 11e > C^d_* + C_* Yes C_7 + C_3 + 9e > C^d_* + C_* No C_7 + C_3 + 10e > C^d_* + C_* Yes C_7 + C_4 + 9e > C^d_* + C_* No C_7 + C_4 + 10e > C^d_* + C_* No C_7 + C_4 + 11e > C^d_* + C_* Yes C_7 + C_5 + 9e > C^d_* + C_* No C_7 + C_5 + 10e > C^d_* + C_* No C_7 + C_5 + 11e > C^d_* + C_* Yes C_7 + C_6 + 9e > C^d_* + C_* No C_7 + C_6 + 10e > C^d_* + C_* No C_7 + C_6 + 11e > C^d_* + C_* No C_7 + C_6 + 12e > C^d_* + C_* Yes C_7 + C_7 + 9e > C^d_* + C_* No C_7 + C_7 + 10e > C^d_* + C_* No C_7 + C_7 + 11e > C^d_* + C_* No C_7 + C_7 + 12e > C^d_* + C_* No C_7 + C_7 + 13e > C^d_* + C_* Yes Lemma 11 C_5 + C_4 + 13e > C^d_* + C^d_* No C_5 + C_4 + 14e > C^d_* + C^d_* Yes C_5 + C_5 + 13e > C^d_* + C^d_* No C_5 + C_5 + 14e > C^d_* + C^d_* No C_5 + C_5 + 15e > C^d_* + C^d_* No C_5 + C_5 + 16e > C^d_* + C^d_* Yes C_6 + C_4 + 13e > C^d_* + C^d_* No C_6 + C_4 + 14e > C^d_* + C^d_* No C_6 + C_4 + 15e > C^d_* + C^d_* No C_6 + C_4 + 16e > C^d_* + C^d_* Yes C_6 + C_5 + 13e > C^d_* + C^d_* No C_6 + C_5 + 14e > C^d_* + C^d_* No C_6 + C_5 + 15e > C^d_* + C^d_* Yes C_6 + C_6 + 13e > C^d_* + C^d_* No C_6 + C_6 + 14e > C^d_* + C^d_* No C_6 + C_6 + 15e > C^d_* + C^d_* No C_6 + C_6 + 16e > C^d_* + C^d_* No C_6 + C_6 + 17e > C^d_* + C^d_* No C_6 + C_6 + 18e > C^d_* + C^d_* No C_6 + C_6 + 19e > C^d_* + C^d_* Yes C_7 + C_4 + 13e > C^d_* + C^d_* No C_7 + C_4 + 14e > C^d_* + C^d_* No C_7 + C_4 + 15e > C^d_* + C^d_* Yes C_7 + C_5 + 13e > C^d_* + C^d_* No C_7 + C_5 + 14e > C^d_* + C^d_* No C_7 + C_5 + 15e > C^d_* + C^d_* No C_7 + C_5 + 16e > C^d_* + C^d_* No C_7 + C_5 + 17e > C^d_* + C^d_* Yes C_7 + C_6 + 13e > C^d_* + C^d_* No C_7 + C_6 + 14e > C^d_* + C^d_* No C_7 + C_6 + 15e > C^d_* + C^d_* No C_7 + C_6 + 16e > C^d_* + C^d_* No C_7 + C_6 + 17e > C^d_* + C^d_* Yes C_7 + C_7 + 13e > C^d_* + C^d_* No C_7 + C_7 + 14e > C^d_* + C^d_* No C_7 + C_7 + 15e > C^d_* + C^d_* No C_7 + C_7 + 16e > C^d_* + C^d_* No C_7 + C_7 + 17e > C^d_* + C^d_* No C_7 + C_7 + 18e > C^d_* + C^d_* Yes Finished