 Later theorem-provers were focused on proof itself rather than a model of human reasoning. By 1960 Hao Wang, Paul Gilmore, and Dag Prawitz had developed computerized theorem-provers for the full first-order predicate calculus (Wang 1960, MacKenzie 1995). In the 1990s William McCune developed Otter, a widely distributed and accessible prover for first-order logic (McCune &amp; Wos 1997, Kalman 2001). A more recent incarnation is Prover9, coupled with search for models and counter-examples in Mace4. Examples of Prover9 derivations are offered in Other Internet Resources. A contemporary alternative is Vampire, developed by Andrei Voronkov, Kryštof Hodere, and Alexander Rizanov (Riazanov &amp; Voronkov 2002).