problem-set/algebra/henkin.models/hp8.desc created : 07/23/86 revised : 07/19/89 Natural Language Description : Theorem HP8: In a Henkin model, for all x, y, and z, if x <= y then x/z <= y/z. Versions : hp8.ver1 : P-formulation, using hyperresolution and UR-resolution. created : 07/09/86. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/17/89. hp8.ver2 : Equality formulation, using paramodulation and UR-resolution. created : 07/09/86. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/18/89. hp8.ver3 : Equality formulation with LE removed, using paramodulation. created : 07/19/89. verified for ITP : untested. translated for OTTER by : caw. verified for OTTER : 07/19/89.