*     modus ponens
new
s all x (man(x) > mortal(x));
s man(Socrates);
q mortal(Socrates);
proof

*   if x is the head of a horse, then x is the head of an animal
new
s all x (horse(x) > animal(x));
q all x (exist y (horse(y) & head(x,y)) > exist z (animal(z) & head(x,z)));
proof

*      did Marcus hate Ceasar?
new
s man(Marcus);
s Pompeian(Marcus);
s all x (Pompeian(x) > Roman(x));
s ruler(Ceasar);
s all x (Roman(x) > hates(x,Ceasar) or loyalto(x,Ceasar));
s all x some y loyalto(x,y);
s all x all y (man(x) & tryassassinate(x,y) & ruler(y) > not loyalto(x,y));
s tryassassinate(Marcus,Ceasar);
q hates(Marcus,Ceasar);
proof

*    existence of a right-identity element
new
s all x all y some z p(z,x,y);
s all x all y some z p(x,z,y);
s all u all v all w all x all y all z
  (p(x,y,u) & p(y,z,v) & p(x,v,w) > p(u,z,w));
q exist x all y p(y,x,y);
proof
eof