A fully automatic problem solver with human-style output. - M. Ganesalingam; W. T. Gowers 001 (CoRR, 2013)

A Fully Automatic Theorem Prover with Human-Style Output. - M. Ganesalingam; W. T. Gowers 001 (J. Autom. Reason., 2017)