<span class="gI">I was experimenting with RACE, and don't understand the results I get below, specifically Subset 3 and Subset 6<br>I can understand that "something" is acting as a name for a constant but when Something = Mary how do I express<br>
the idea that the substitution is under the constraint of being male ?<br><br></span><div class="in"><p><b>Axioms</b>: Every man is a human. Every woman is a human. 
Mary is a woman. John is a man. Fido is a dog.
No dog is a human. John is a male. Fido is a male.
</p><p><b>Theorems</b>: Something is a male.</p><p><b>Parameters</b>: </p></div><p>The following minimal subsets of the axioms entail the theorems:</p><ul><li>Subset 1<ul><li>7: John is a male.</li><li>Substitution: something = Fido</li>
</ul></li><li>Subset 2<ul><li>7: John is a male.</li><li>Substitution: something = John</li></ul></li><li>Subset 3<ul><li>7: John is a male.</li><li>Substitution: something = Mary</li></ul></li><li>Subset 4<ul><li>8: Fido is a male.</li>
<li>Substitution: something = Fido</li></ul></li><li>Subset 5<ul><li>8: Fido is a male.</li><li>Substitution: something = John</li></ul></li><li>Subset 6<ul><li>8: Fido is a male.</li><li>Substitution: something = Mary</li>
</ul></li></ul><div class="infoBox">overall time: 1.75 sec; RACE time: 0.16 sec</div><br>