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

% CUP-2.IN                 1999 March 4

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


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Mar 04 20:27:00 1999

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

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

82 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
307 [] subclass(cart(cart(x,y),z),cart(cart(V,V),V)).
752 [] subclass(composite(x,y),cart(D(y),R(x))).
1381 [] subclass(PSM(x),x).
2632 [] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP).
2633 [] -subclass(CUP,cart(cart(V,V),V)).
2736 [] equal(R(inverse(x)),D(x)).
2870 [] equal(D(S),V).
3272 [] equal(D(DUP),V).
3301 [] equal(D(cross(x,y)),cart(D(x),D(y))).
3481 [para_into,2633.1.1,2632.1.2] 
          -subclass(PSM(composite(inverse(DUP),cross(S,S))),
          cart(cart(V,V),V)).
3497 [ur,3481,82,1381] 
          -subclass(composite(inverse(DUP),cross(S,S)),
          cart(cart(V,V),V)).
3540 [ur,3497,82,752,demod,3301,2870,2870,2736,3272] 
          -subclass(cart(cart(V,V),V),cart(cart(V,V),V)).
3541 [binary,3540.1,307.1] $F.

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

clauses generated   11240
Kbytes malloced      2458
user CPU time          13.24  seconds