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

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

formula_list(sos).
% negation of Theorem CR-1
-(all x subclass(compreln(x),cart(V,V))).
end_of_list.


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

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

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

241 [] subclass(restrict(x,y,z),cart(y,z)).
262 [] equal(restrict(complement(x),V,V),compreln(x)).
263 [] -subclass(compreln($c1),cart(V,V)).
307 [para_into,263.1.1,262.1.2] 
          -subclass(restrict(complement($c1),V,V),cart(V,V)).
308 [binary,307.1,241.1] $F.

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

clauses generated       1
Kbytes malloced       287
user CPU time           0.61  seconds