----- SUMMARY FOR THEOREM CR-3 IN DIRECTORY Q:\CR -----

% CR-3.IN                  Created 1995 September 11
% Complementary Relation 

formula_list(sos).
% negation of Theorem CR-3
-(all x subclass(compreln(x),complement(x))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Jul 13 22:35:44 1997

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

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

253 [] -disjoint(x,complement(y)) | subclass(x,y).
264 [] disjoint(compreln(x),x).
265 [] -subclass(compreln($c1),complement($c1)).
278 [] equal(complement(complement(x)),x).
309 [ur,265,253,demod,278] -disjoint(compreln($c1),$c1).
310 [binary,309.1,264.1] $F.

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

clauses generated       1
Kbytes malloced       287
user CPU time           0.49  seconds