<div dir="ltr"><br><div class="gmail_quote"><div dir="ltr"><div><div><div>Norbert,<br></div>thank you for the hard work on RACE.<br></div>I did use the interface at <a href="http://attempto.ifi.uzh.ch/race/" target="_blank">http://attempto.ifi.uzh.ch/race/</a><br></div>and got results that I expected:<br><br><div><p><b>Axioms</b>: Every man is a human. Every woman is a human. 
Mary is a woman. John is a man. Kelly is a human.
if a human is not provably a woman then the human is a man.

</p><p><b>Theorems</b>: Kelly is a woman.</p><p><b>Parameters</b>: </p></div><p>Theorems do not follow from axioms.</p><div>overall time: 0.585 sec; RACE time: 0.024 sec</div><div><p><b>Axioms</b>: Every man is a human. Every woman is a human. 
Mary is a woman. John is a man. Kelly is a human.
if a human is not provably a woman then the human is a man.

</p><p><b>Theorems</b>: Kelly is a man.</p><p><b>Parameters</b>: </p></div><p>The following minimal subsets of the axioms entail the theorems:</p>Subset 1<ul><li>5: Kelly is a human.</li><span class=""><li>6: If a human is not provably a woman then the human is a man.</li></span></ul><br></div><div>Thanks again,<br></div><div>David<br></div></div></div>