----- Otter 3.0.4, August 1995 -----
The job was started by Macintosh user on a Macintosh, 
Sun Oct  8 19:31:57 2000
The command was "OTTER 3.0.4".

set(auto).

    ...

formula_list(usable).

-((all x P(x))-> (exists y P(y))).

end_of_list.

-------> usable clausifies to:

list(usable).
0 [] P(x).
0 [] -P(y).
end_of_list.

    ...


This is a Horn set without equality.  The strategy will
be hyperresolution, with satellites in sos and nuclei
in usable.

    ...

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

1 [] -P(x).
2 [] P(x).
3 [binary,2.1,1.1] $F.

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