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

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

formula_list(sos).
% negation of Theorem CR-4
-(all x equal(compreln(restrict(x,V,V)),compreln(x))).
end_of_list.


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

Length of proof is 5. Level of proof is 5.

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

30 [] equal(restrict(xr,x,y),intersection(xr,cart(x,y))).
195 [] equal(intersection(x,union(y,z)),union(intersection(x,y),
          intersection(x,z))).
262 [] equal(restrict(complement(x),V,V),compreln(x)).
266 [] -equal(compreln(restrict($c1,V,V)),compreln($c1)).
267 [] equal(intersection(x,y),intersection(y,x)).
283 [] equal(intersection(complement(x),x),0).
287 [] equal(complement(intersection(x,y)),
          union(complement(x),complement(y))).
290 [] equal(union(0,x),x).
311 [para_into,266.1.1,262.1.2] 
          -equal(restrict(complement(restrict($c1,V,V)),
          V,V),compreln($c1)).
313 [para_into,311.1.1,30.1.1] 
          -equal(intersection(complement(restrict($c1,V,V)),
          cart(V,V)),compreln($c1)).
314 [para_into,313.1.1.1.1,30.1.1,demod,267,287,267] 
          -equal(intersection(cart(V,V),union(complement(cart(V,V)),
          complement($c1))),compreln($c1)).
315 [para_into,314.1.1,195.1.1,demod,267,283,267,290] 
          -equal(intersection(complement($c1),cart(V,V)),
          compreln($c1)).
316 [para_into,315.1.1,30.1.2] 
          -equal(restrict(complement($c1),V,V),compreln($c1)).
317 [binary,316.1,262.1] $F.

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

clauses generated      66
Kbytes malloced       319
user CPU time           0.66  seconds