 These possible colorings were logically and algorithmically narrowed down to around a trillion (still highly complex) cases, and those were examined using a Boolean satisfiability solver.Creating the proof took about 4 CPU-years of computation over a period of two days on the Stampede supercomputer at the Texas Advanced Computing Center and generated a 200 terabyte propositional proof, which was compressed to 68 gigabytes.The paper describing the proof was published in the SAT 2016 conference, where it won the best paper award.