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

% H-FULL-1.IN                 2001 March 22
% Restatement of Theorem FUL-LIM2 in the FUL\3 group.

formula_list(sos).
% negation of Corollary H-FULL-1
-equal(H(FULL),intersection(FULL,P(FULL))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Mar 22 08:55:53 2001

Length of proof is 1. Level of proof is 1.

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

78 [] equal(x,x).
3292 [] equal(U(intersection(FULL,P(FULL))),
          intersection(FULL,P(FULL))).
3720 [] -equal(H(FULL),intersection(FULL,P(FULL))).
4908 [] equal(U(intersection(FULL,P(x))),H(x)).
4909 [para_into,3720.1.2,3292.1.2,demod,4908] 
          -equal(H(FULL),H(FULL)).
4910 [binary,4909.1,78.1] $F.

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

clauses generated      67
Kbytes malloced      3480
user CPU time           2.86  seconds