[Attempto] Question about http://attempto.ifi.uzh.ch/race/

[David Whitten]

I was experimenting with RACE, and don't understand the results I get
below, specifically Subset 3 and Subset 6
I can understand that "something" is acting as a name for a constant but
when Something = Mary how do I express
the idea that the substitution is under the constraint of being male ?

*Axioms*: 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.

*Theorems*: Something is a male.

*Parameters*:

The following minimal subsets of the axioms entail the theorems:

   - Subset 1
      - 7: John is a male.
      - Substitution: something = Fido
   - Subset 2
      - 7: John is a male.
      - Substitution: something = John
   - Subset 3
      - 7: John is a male.
      - Substitution: something = Mary
   - Subset 4
      - 8: Fido is a male.
      - Substitution: something = Fido
   - Subset 5
      - 8: Fido is a male.
      - Substitution: something = John
   - Subset 6
      - 8: Fido is a male.
      - Substitution: something = Mary

overall time: 1.75 sec; RACE time: 0.16 sec
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20120412/00c7eb0b/attachment.html>