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

% CUP-OP3A.IN                 1999 July 22

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


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

Length of proof is 12. Level of proof is 6.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
81 [] subclass(x,x).
185 [] -member(x,y) | -member(x,z) | -disjoint(y,z).
252 [] member(pair(x,y),V).
292 [] subclass(cart(x,y),cart(V,V)).
499 [] -member(x,y) | -member(pair(x,z),u)
           | -subclass(u,cart(V,V)) | member(z,image(u,y)).
746 [] -member(pair(x,y),z) | -member(pair(x,y),cart(V,V))
           | -member(pair(y,u),v) | -member(pair(y,u),cart(V,V))
           | member(pair(x,u),composite(v,z)).
754 [] subclass(composite(x,y),cart(V,R(x))).
1288 [] -member(x,y) | -subclass(z,x) | member(z,image(inverse(S),
          y)).
1399 [] subclass(PS,cart(V,V)).
1403 [] -member(x,V) | -subclass(y,x) | equal(y,x)
           | member(pair(y,x),PS).
1414 [] subclass(PSM(x),x).
1415 [] disjoint(PSM(x),composite(PS,x)).
2033 [] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP).
2034 [] subclass(CUP,cart(V,V)).
2036 [] -subclass(union(x,y),z) | -member(z,V)
           | member(pair(pair(x,y),z),composite(inverse(DUP),
          cross(S,S))).
2037 [] -member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S)))
           | subclass(union(x,y),z).
2038 [] member(pair(pair($c3,$c2),$c1),CUP).
2039 [] -equal(union($c3,$c2),$c1).
2140 [] equal(R(inverse(x)),D(x)).
2146 [] equal(R(cart(x,x)),x).
2155 [] equal(image(x,V),R(x)).
2275 [] equal(D(S),V).
2698 [] equal(D(DUP),V).
2739 [ur,2038,1,2034] member(pair(pair($c3,$c2),$c1),cart(V,V)).
2740 [para_into,2038.1.2,2033.1.2] 
          member(pair(pair($c3,$c2),$c1),PSM(composite(inverse(DUP),
          cross(S,S)))).
2745 [ur,2739,499,252,292,demod,2155,2146] member($c1,V).
2746 [ur,2740,185,1415] 
          -member(pair(pair($c3,$c2),$c1),
          composite(PS,composite(inverse(DUP),cross(S,S)))).
2747 [ur,2740,1,1414] 
          member(pair(pair($c3,$c2),$c1),composite(inverse(DUP),
          cross(S,S))).
2752 [ur,2747,2037] subclass(union($c3,$c2),$c1).
2756 [ur,2752,1403,2745,2039] member(pair(union($c3,$c2),$c1),PS).
2757 [ur,2752,1288,2745,demod,2155,2140,2275] 
          member(union($c3,$c2),V).
2770 [ur,2756,1,1399] member(pair(union($c3,$c2),$c1),cart(V,V)).
2772 [ur,2757,2036,81] 
          member(pair(pair($c3,$c2),union($c3,$c2)),
          composite(inverse(DUP),cross(S,S))).
2802 [ur,2772,746,2756,2770,2746] 
          -member(pair(pair($c3,$c2),union($c3,$c2)),cart(V,V)).
2803 [ur,2772,1,754,demod,2140,2698] 
          member(pair(pair($c3,$c2),union($c3,$c2)),cart(V,V)).
2804 [binary,2803.1,2802.1] $F.

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

clauses generated   33869
Kbytes malloced      2011
user CPU time           4.50  seconds