you don't need to work that hard - see

Computers & Mathematics with Applications

Volume 34, Issue 11, December 1997, Pages 1–8

Biplanar Graphs:: A Survey

L.W. Beineke

the first paragraphs are about k_9

you might also be able to make a counting argument, since k_9 has 36 edges and any decomposition into two parts has at least 18 edges in one or the other part (so you might be able to prove a K_3,3 or K_5 must be in one part or the other)

none of this proves that the 4-color theorem cannot be used, but there are other possibilities

I have already studied, that paper of Beineke. I also gone through the original works of J Battle et. al., and that of Tutte. In this topic, Harary wrote in his book, "No elegant or even reasonable proof is known" in relation to the nonplanarity of K_9.