problem-set/geometry/tarski/t9.desc created : 07/16/86 revised : 08/17/89 Natural Language Description : Theorem 9: For all points x, y, z, and w, if y and w are between x and z, then either y is between x and w or w is between x and y. Versions : NOTE: all versions use a weighting scheme in which variables (and skolem functions) are weighted high and constants low. t9.ver1 : Original formulation of the axioms, from McCharen, Overbeek, & Wos [Aug. 1976]. created : 07/16/86. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : no proof. t9.ver2 : Reformulation of the axioms, from Quaife [JAR 5 (1989)]. created : 07/25/89. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : no proof. t9.ver3 : Reformulation of the axioms, from Quaife [JAR 5 (1989)]. created : 07/25/89. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : no proof.