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

% CUP-FU.IN                 1999 July 22
% CUP is a function.

formula_list(sos).
% negation of Theorem CUP-FU
-FUNCTION(CUP).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Jul 22 13:13:15 1999

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

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

1072 [] -equal(sv2(x),sv1(x)) | SINGLEVALUED(x).
1073 [] SINGLEVALUED(x) | member(pair(sv3(x),sv1(x)),x).
1074 [] SINGLEVALUED(x) | member(pair(sv3(x),sv2(x)),x).
1090 [] -SINGLEVALUED(x) | -subclass(x,cart(V,V)) | FUNCTION(x).
2075 [] subclass(CUP,cart(V,V)).
2080 [] -member(pair(x,y),CUP) | equal(union(first(x),second(x)),y).
2082 [] -FUNCTION(CUP).
2784 [ur,2082,1090,2075] -SINGLEVALUED(CUP).
2789 [ur,2784,1074] member(pair(sv3(CUP),sv2(CUP)),CUP).
2790 [ur,2784,1073] member(pair(sv3(CUP),sv1(CUP)),CUP).
2791 [ur,2784,1072] -equal(sv2(CUP),sv1(CUP)).
2809,2808 [ur,2789,2080,flip.1] 
          equal(sv2(CUP),union(first(sv3(CUP)),second(sv3(CUP)))).
2811 [back_demod,2791,demod,2809,flip.1] 
          -equal(sv1(CUP),union(first(sv3(CUP)),second(sv3(CUP)))).
2812 [ur,2790,2080,flip.1] 
          equal(sv1(CUP),union(first(sv3(CUP)),second(sv3(CUP)))).
2814 [binary,2812.1,2811.1] $F.

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

clauses generated    3699
Kbytes malloced      2043
user CPU time           2.03  seconds