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

% CUP-AP1.IN                 2000 August 17

formula_list(sos).
% negation of Corollary CUP-AP2
-(all x (member(x,cart(V,V)) -> 
           equal(apply(CUP,x),union(first(x),second(x))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Aug 17 12:20:42 2000

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

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

15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x).
83 [] equal(x,x).
2185 [] -member(pair(x,y),cart(V,V)) | equal(apply(CUP,pair(x,y)),
          union(x,y)).
2186 [] member($c1,cart(V,V)).
2187 [] -equal(apply(CUP,$c1),union(first($c1),second($c1))).
2954,2953 [ur,2186,15] equal(pair(first($c1),second($c1)),$c1).
2955 [para_into,2187.1.2,2185.2.2,demod,2954,2954,unit_del,83,2186] 
          $F.

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

clauses generated    1738
Kbytes malloced      2139
user CPU time           1.76  seconds