 Neither Huntington nor Robbins could prove this, and later it withstood the efforts of many others, including even Tarski and his talented school at Berkeley. Building on partial results of Winker, the automated theorem prover EQP, designed by William McCune of the Argonne National Laboratory, found a proof of the Robbins Conjecture in 1996. This accomplishment was popularized in Kolata 2010.