----- SUMMARY FOR THEOREM H-1 IN DIRECTORY Q:\h -----

% H-1.IN                 2001 March 13
% Jech's hereditarily constructor

formula_list(sos).
% negation of Theorem H-1
-(all x full(H(x))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Mar 18 23:08:03 2001

Length of proof is 2. Level of proof is 2.

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

93 [] subclass(intersection(x,y),x).
3272 [] -subclass(x,FULL) | full(U(x)).
3719 [] equal(U(intersection(FULL,P(x))),H(x)).
3720 [] -full(H($c1)).
4910 [para_into,3720.1.1,3719.1.2] 
          -full(U(intersection(FULL,P($c1)))).
4920 [ur,4910,3272] -subclass(intersection(FULL,P($c1)),FULL).
4921 [binary,4920.1,93.1] $F.

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

clauses generated     311
Kbytes malloced      3480
user CPU time           2.80  seconds