Socrates is Mortal Example (CHUG)

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
   end_of_list.

Output:

  =========== start of search ===========

  given clause #1: (wt=2) 2 [] man(socrates).

  given clause #2: (wt=2) 3 [hyper,2,1] mortal(socrates).

  Search stopped because sos empty.


  Search stopped because sos empty.

  ============ end of search ===========