problem-set/algebra/category.theory/p1.desc created : 07/09/86 revised : 07/19/89 Natural Language Description: Theorem 1: If xy is a monomorphism, then y is a monomorphism. Versions : p1.ver1 : uses UR resolution, with axioms from B.Mitchell, "Theory of Categories", Chapter 1. created : from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : 07/11/86, no proof. translated for OTTER by : caw. verified for OTTER : 07/07/89. p1.ver2 : Quaife axioms, using UR resolution, paramodulation into the given clause, and dynamic demodulation; created : from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : no proof. p1.ver3 : Scott axioms, using UR resolution. created : from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/10/89.