----- SUMMARY FOR THEOREM CUP-AP1 IN DIRECTORY Q:\cup -----

% CUP-AP1.IN                 1999 August 11

formula_list(sos).
% negation of Theorem CUP-AP1
-(all x y (member(pair(x,y),cart(V,V)) -> 
           equal(apply(CUP,pair(x,y)),union(x,y)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Aug 12 14:16:37 1999

Length of proof is 4. Level of proof is 4.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
1093 [] -FUNCTION(x) | SINGLEVALUED(x).
1640 [] -SINGLEVALUED(x) | -member(pair(y,z),x)
           | -member(pair(y,z),cart(V,V)) | equal(apply(x,y),z).
2099 [] subclass(CUP,cart(V,V)).
2106 [] -member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)),
          CUP).
2107 [] FUNCTION(CUP).
2108 [] member(pair($c2,$c1),cart(V,V)).
2109 [] -equal(apply(CUP,pair($c2,$c1)),union($c2,$c1)).
2847 [ur,2108,2106] member(pair(pair($c2,$c1),union($c2,$c1)),CUP).
2853 [ur,2847,1,2099] 
          member(pair(pair($c2,$c1),union($c2,$c1)),cart(V,V)).
2872 [ur,2853,1640,2847,2109] -SINGLEVALUED(CUP).
2906 [ur,2872,1093] -FUNCTION(CUP).
2907 [binary,2906.1,2107.1] $F.

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

clauses generated   50082
Kbytes malloced      2075
user CPU time           8.52  seconds