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

% CUP-OP4.IN                 1999 July 22

formula_list(sos).
% negation of Theorem CUP-OP4
-(all x y (member(pair(x,y),cart(V,V)) ->
           member(pair(pair(x,y),union(x,y)),CUP))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Jul 22 12:28:23 1999

Length of proof is 13. Level of proof is 8.

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

5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
21 [] -member(x,y) | -member(x,z) | member(x,intersection(y,z)).
81 [] subclass(x,x).
293 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
603 [] -member(pair(x,y),cart(V,V)) | member(union(x,y),V).
779 [] -member(pair(x,y),composite(z,u))
           | member(pair(x,com(z,u,x,y)),u).
781 [] -member(pair(x,y),composite(z,u))
           | member(pair(com(z,u,x,y),y),z).
1401 [] -member(pair(x,x),PS).
1402 [] -member(pair(x,y),PS) | subclass(x,y).
1413 [] equal(intersection(x,complement(composite(PS,x))),PSM(x)).
1778 [] -member(x,cart(V,V)) | member(x,y)
           | member(x,restrict(complement(y),V,V)).
2033 [] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP).
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($c2,$c1),cart(V,V)).
2039 [] -member(pair(pair($c2,$c1),union($c2,$c1)),CUP).
2071 [] equal(complement(complement(x)),x).
2308 [] equal(restrict(x,V,V),composite(Id,x)).
2318 [] equal(composite(Id,composite(x,y)),composite(x,y)).
2739 [ur,2038,603] member(union($c2,$c1),V).
2743 [para_into,2039.1.2,2033.1.2] 
          -member(pair(pair($c2,$c1),union($c2,$c1)),
          PSM(composite(inverse(DUP),cross(S,S)))).
2745 [ur,2739,2036,81] 
          member(pair(pair($c2,$c1),union($c2,$c1)),
          composite(inverse(DUP),cross(S,S))).
2751 [ur,2739,293,2038] 
          member(pair(pair($c2,$c1),union($c2,$c1)),cart(V,V)).
2767 [para_into,2743.1.2,1413.1.2] 
          -member(pair(pair($c2,$c1),union($c2,$c1)),
          intersection(composite(inverse(DUP),cross(S,S)),
          complement(composite(PS,composite(inverse(DUP),
          cross(S,S)))))).
2796 [ur,2767,21,2745] 
          -member(pair(pair($c2,$c1),union($c2,$c1)),
          complement(composite(PS,composite(inverse(DUP),
          cross(S,S))))).
2869 [ur,2796,1778,2751,demod,2071,2308,2318] 
          member(pair(pair($c2,$c1),union($c2,$c1)),
          composite(PS,composite(inverse(DUP),cross(S,S)))).
2946 [ur,2869,781] member(pair(com(PS,composite(inverse(DUP),cross(S,S)),
          pair($c2,$c1),union($c2,$c1)),union($c2,$c1)),PS).
2948 [ur,2869,779] member(pair(pair($c2,$c1),
          com(PS,composite(inverse(DUP),cross(S,S)),
          pair($c2,$c1),union($c2,$c1))),composite(inverse(DUP),
          cross(S,S))).
3060 [ur,2946,1402] subclass(com(PS,composite(inverse(DUP),cross(S,S)),
          pair($c2,$c1),union($c2,$c1)),union($c2,$c1)).
3061 [ur,2948,2037] subclass(union($c2,$c1),
          com(PS,composite(inverse(DUP),cross(S,S)),
          pair($c2,$c1),union($c2,$c1))).
3227,3226 [ur,3061,5,3060] 
          equal(com(PS,composite(inverse(DUP),cross(S,S)),
          pair($c2,$c1),union($c2,$c1)),union($c2,$c1)).
3228 [back_demod,2946,demod,3227] 
          member(pair(union($c2,$c1),union($c2,$c1)),PS).
3229 [binary,3228.1,1401.1] $F.

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

clauses generated  193347
Kbytes malloced      2363
user CPU time          42.90  seconds