fof(0, conjecture, mortal(socrates)).
fof(1, axiom, ! [Y]: (human(Y) => mortal(Y))).
fof(2, axiom, human(socrates)).