----- SUMMARY FOR THEOREM cup-in3 IN DIRECTORY Q:\cup -----

% CUP-IN3.IN                 2001 September 4

formula_list(sos).
% negation of Theorem CUP-IN3
-(all x y z (member(pair(x,y),image(inverse(CUP),singleton(z))) ->
             equal(union(x,y),z))).     
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Tue Sep 04 21:41:28 2001

Length of proof is 3. Level of proof is 2.

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

422 [] -member(pair(x,y),inverse(z)) | member(pair(y,x),z).
507 [] -member(x,image(y,singleton(z))) | member(pair(z,x),y).
2699 [] -member(pair(pair(x,y),z),CUP) | equal(union(x,y),z).
2702 [] member(pair($c3,$c2),image(inverse(CUP),singleton($c1))).
2703 [] -equal(union($c3,$c2),$c1).
3589 [ur,2702,507] member(pair($c1,pair($c3,$c2)),inverse(CUP)).
3591 [ur,2703,2699] -member(pair(pair($c3,$c2),$c1),CUP).
3593 [ur,3589,422] member(pair(pair($c3,$c2),$c1),CUP).
3594 [binary,3593.1,3591.1] $F.

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

clauses generated    5452
Kbytes malloced      2650
user CPU time          14.01  seconds