problem-set/geometry/tarski/t11.desc created : 07/16/86 revised : 07/28/89 Natural Language Description : Theorem 11: The three points C1, C2, C3 specified in the axiom set are NOT collinear. Versions : NOTE: all versions use a weighting scheme in which variables (and skolem functions) are weighted high and constants low. t11.ver1 : Original formulation of the axioms, from McCharen, Overbeek, & Wos [Aug. 1976]; uses hyperresolution, UR resolution, and unit deletion. created : 07/16/86. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/20/89. t11.ver2 : Reformulation of the axioms, from Quaife [JAR 5 (1989)]; uses hyperresolution and unit deletion. created : 07/25/89. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/27/89. t11.ver3 : Reformulation of the axioms, from Quaife [JAR 5 (1989)]; uses hyperresolution and unit deletion. created : 07/25/89. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/27/89.