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

% CUP-3.IN                 1999 July 22

formula_list(sos).
% negation of Theorem CUP-3
-subclass(D(CUP),cart(V,V)).
end_of_list.


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

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

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

82 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
377 [] -subclass(x,y) | subclass(D(x),D(y)).
382 [] subclass(D(cart(x,y)),x).
2076 [] subclass(CUP,cart(cart(V,V),V)).
2077 [] -subclass(D(CUP),cart(V,V)).
2811 [ur,2077,82,382] -subclass(D(CUP),D(cart(cart(V,V),x))).
2838 [ur,2811,377] -subclass(CUP,cart(cart(V,V),x)).
2839 [binary,2838.1,2076.1] $F.

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

clauses generated    2208
Kbytes malloced      2043
user CPU time           1.70  seconds