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

% CR-7.IN                  1997 November 30
% Complementary Relation 

formula_list(sos).
% negation of Theorem CR-7
-(all x y equal(compreln(intersection(x,y)),
                union(compreln(x),compreln(y)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Nov 30 13:18:36 1997

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

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

117 [] equal(x,x).
238,237 [] equal(complement(intersection(x,y)),
          union(complement(x),complement(y))).
397,396 [] equal(restrict(union(x,y),z,u),
          union(restrict(x,z,u),restrict(y,z,u))).
421,420 [] equal(restrict(complement(x),V,V),compreln(x)).
434 [] -equal(compreln(intersection($c2,$c1)),
          union(compreln($c2),compreln($c1))).
437 [para_into,434.1.1,420.1.2,demod,238,397,421,421] 
          -equal(union(compreln($c2),compreln($c1)),
          union(compreln($c2),compreln($c1))).
438 [binary,437.1,117.1] $F.

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

clauses generated      37
Kbytes malloced       574
user CPU time           1.64  seconds