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

% CUP-ADJ'.IN                 2000 April 7
% More general lemma needed for FINITE induction.

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


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Apr 07 22:53:15 2000

Length of proof is 7. Level of proof is 3.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
4 [] subclass(x,V).
14 [] member(pair(u,v),cart(x,y)) | -member(u,x) | -member(v,y).
292 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
500 [] -member(x,y) | -member(pair(x,z),u)
           | -subclass(u,cart(V,V)) | member(z,image(u,y)).
1251 [] -member(x,y) | member(singleton(x),image(SINGLETON,y)).
2259 [] subclass(CUP,cart(V,V)).
2265 [] -member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)),
          CUP).
2266 [] member($c3,$c1).
2267 [] member($c2,$c4).
2268 [] subclass(image(CUP,cart($c1,image(SINGLETON,$c4))),$c1).
2269 [] -member(union($c3,singleton($c2)),$c1).
3035 [ur,2266,1,4] member($c3,V).
3036 [ur,2267,1251] member(singleton($c2),image(SINGLETON,$c4)).
3044 [ur,2269,1,2268] 
          -member(union($c3,singleton($c2)),
          image(CUP,cart($c1,image(SINGLETON,$c4)))).
3050 [ur,3036,292,3035] member(pair($c3,singleton($c2)),cart(V,V)).
3057 [ur,3036,14,2266] 
          member(pair($c3,singleton($c2)),
          cart($c1,image(SINGLETON,$c4))).
3087 [ur,3050,2265] member(pair(pair($c3,singleton($c2)),
          union($c3,singleton($c2))),CUP).
3107 [ur,3057,500,2259,3044] 
          -member(pair(pair($c3,singleton($c2)),
          union($c3,singleton($c2))),CUP).
3108 [binary,3107.1,3087.1] $F.

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

clauses generated   48138
Kbytes malloced      2235
user CPU time           8.01  seconds