----- SUMMARY FOR THEOREM CUP-SUB' IN DIRECTORY Q:\cup -----

% CUP-SUB'.IN                 2000 March 21
% Slightly more general subtractive form similar to CUP-SUB

formula_list(sos).
% negation of Theorem CUP-SUB'
-(all w x y z ((member(x,y) & subclass(y,w) &
               member(intersection(y,complement(singleton(x))),z) &
              subclass(image(CUP,cart(z,image(SINGLETON,w))),z)) ->
              member(y,z))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Apr 08 20:45:50 2000

Length of proof is 14. Level of proof is 6.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
4 [] subclass(x,V).
23 [] -member(x,V) | member(x,y) | member(x,complement(y)).
94 [] subclass(intersection(x,y),y).
101 [] equal(intersection(x,y),intersection(y,x)).
122 [] -member(x,union(y,z)) | member(x,y) | member(x,z).
123 [] -member(x,y) | member(x,union(y,z)).
165 [] equal(union(x,intersection(x,y)),x).
175 [] subclass(union(x,intersection(y,z)),union(x,z)).
181 [] -member(x,y) | -member(x,z) | -disjoint(y,z).
185 [] disjoint(complement(x),x).
218 [] -member(x,complement(singleton(x))).
238 [] -member(x,y) | -subclass(y,singleton(x))
           | equal(singleton(x),y).
2267 [] -member(x,z) | -member(y,w) | member(union(x,singleton(y)),z)
           | -subclass(image(CUP,cart(z,image(SINGLETON,w))),z).
2268 [] member($c3,$c2).
2269 [] subclass($c2,$c4).
2270 [] member(intersection($c2,complement(singleton($c3))),$c1).
2271 [] subclass(image(CUP,cart($c1,image(SINGLETON,$c4))),$c1).
2272 [] -member($c2,$c1).
2304 [] equal(complement(complement(x)),x).
2309 [] equal(complement(union(x,y)),intersection(complement(x),
          complement(y))).
2319 [] equal(union(x,y),union(y,x)).
2325 [] equal(union(x,intersection(complement(x),y)),union(x,y)).
3036 [ur,2268,181,185] -member($c3,complement($c2)).
3039 [ur,2268,1,4] member($c3,V).
3046 [ur,2269,1,2268] member($c3,$c4).
3051 [para_into,2270.1.1,101.1.2] 
          member(intersection(complement(singleton($c3)),$c2),$c1).
3052 [ur,2272,122,218,demod,2319] 
          -member($c2,union($c1,complement(singleton($c2)))).
3055 [ur,3036,122,218,demod,2319] 
          -member($c3,union(complement($c2),
          complement(singleton($c3)))).
3118 [ur,3051,2267,3046,2271,demod,2319,2325,2319] 
          member(union($c2,singleton($c3)),$c1).
3122 [ur,3052,1,175] -member($c2,union($c1,
          intersection(x,complement(singleton($c2))))).
3127 [ur,3055,23,3039,demod,2309,2304,2304] 
          member($c3,intersection($c2,singleton($c3))).
3265 [ur,3118,123] member(union($c2,singleton($c3)),union($c1,x)).
3267 [para_into,3122.1.2.2,101.1.2] 
          -member($c2,union($c1,intersection(complement(singleton($c2)),
          x))).
3269,3268 [ur,3127,238,94,flip.1] 
          equal(intersection($c2,singleton($c3)),singleton($c3)).
3459,3458 [para_from,3268.1.1,165.1.1.2] 
          equal(union($c2,singleton($c3)),$c2).
3467 [para_from,3268.1.2,3265.1.1.2,demod,3269,3459] 
          member($c2,union($c1,x)).
3468 [binary,3467.1,3267.1] $F.

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

clauses generated  253768
Kbytes malloced      2426
user CPU time          23.40  seconds