Socrates is Mortal Example (Contradiction)

Input:

   set(auto).
   formula_list(usable).
     all x (man(x)->mortal(x)).    % For all x, if x is a man then x is mortal
     man(socrates).                % Socrates is a man
     -mortal(socrates).		   % Socrates is immortal
   end_of_list.

Output:

  ---------------- PROOF ----------------

  1 [] -man(x)|mortal(x).
  2 [] -mortal(socrates).
  3 [] man(socrates).
  4 [hyper,3,1] mortal(socrates).
  5 [binary,4.1,2.1] $F.

  ------------ end of proof -------------