"The negative witness, that is, the DRUP unsatisfiability certificate, is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so one may have doubts about to which degree this can be accepted as a proof of a mathematical statement." http://gowers.wordpress.com/2014/02/11/recent-news-concerning-the-erdos-disc... -- Thane Plambeck tplambeck@gmail.com http://counterwave.com/