fof(wealldie,      axiom, ![X]:(human(X) => mortal(X))).
fof(socrateshuman, axiom, ![X]:(human(socrates))).
fof(socratesdies,  conjecture, mortal(socrates)).