fof(axiom1, axiom, ![X]: (human(X) => mortal(X))).
fof(axiom2, axiom, human(socrates)).
fof(conjecture, conjecture, mortal(socrates)).