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

% CUP-PC-2.IN                 2000 July 20

formula_list(sos).
% negation of Theorem CUP-PC-2
-(all x y equal(image(CUP,cart(P(x),P(y))),P(union(x,y)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Jul 21 01:25:32 2000

Length of proof is 15. Level of proof is 9.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
14 [] member(pair(u,v),cart(x,y)) | -member(u,x) | -member(v,y).
94 [] subclass(intersection(x,y),y).
137 [] -subclass(x,y) | equal(intersection(x,y),x).
447 [] -member(pair(x,y),z) | -member(pair(x,y),cart(V,V))
           | member(y,R(z)).
500 [] -member(x,y) | -member(pair(x,z),u)
           | -subclass(u,cart(V,V)) | member(z,image(u,y)).
645 [] -member(x,P(y)) | subclass(x,y).
646 [] -member(x,V) | -subclass(x,y) | member(x,P(y)).
903 [] subclass(x,image(S,x)).
1217 [] equal(image(id(x),y),intersection(x,y)).
1373 [] -member(union(x,y),V) | member(x,V).
1375 [] -member(union(x,y),V) | member(pair(x,y),cart(V,V)).
2324 [] subclass(CUP,cart(V,V)).
2330 [] -member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)),
          CUP).
2331 [] subclass(image(CUP,cart(P(x),P(y))),P(union(x,y))).
2332 [] -equal(image(CUP,cart(P($c2),P($c1))),P(union($c2,$c1))).
2439 [] equal(R(cart(x,x)),x).
2450 [] equal(image(x,union(y,z)),union(image(x,y),image(x,z))).
2574 [] equal(image(S,P(x)),V).
2703 [] equal(image(id(x),y),intersection(x,y)).
3114 [] equal(notsub(P(union(x,y)),image(CUP,cart(P(x),P(y)))),
          n$(x,y)).
3115 [ur,2332,5,2331] 
          -subclass(P(union($c2,$c1)),image(CUP,cart(P($c2),
          P($c1)))).
3117 [ur,3115,3,demod,3114] 
          -member(n$($c2,$c1),image(CUP,cart(P($c2),P($c1)))).
3118 [ur,3115,2,demod,3114] member(n$($c2,$c1),P(union($c2,$c1))).
3120 [ur,3118,645] subclass(n$($c2,$c1),union($c2,$c1)).
3122 [ur,3118,1,903,demod,2574] member(n$($c2,$c1),V).
3124 [ur,3120,137] equal(intersection(n$($c2,$c1),union($c2,$c1)),
          n$($c2,$c1)).
3131,3130 [para_into,3124.1.1,1217.1.2,demod,2450,2703,2703] 
          equal(union(intersection(n$($c2,$c1),
          $c2),intersection(n$($c2,$c1),$c1)),n$($c2,$c1)).
3141 [para_from,3130.1.1,1375.1.1,unit_del,3122] 
          member(pair(intersection(n$($c2,$c1),
          $c2),intersection(n$($c2,$c1),$c1)),cart(V,V)).
3142 [para_from,3130.1.1,1373.1.1,unit_del,3122] 
          member(intersection(n$($c2,$c1),$c2),V).
3145 [ur,3141,2330,demod,3131] 
          member(pair(pair(intersection(n$($c2,$c1),
          $c2),intersection(n$($c2,$c1),$c1)),n$($c2,$c1)),CUP).
3149 [ur,3141,447,3141,demod,2439] 
          member(intersection(n$($c2,$c1),$c1),V).
3154 [ur,3142,646,94] member(intersection(n$($c2,$c1),$c2),P($c2)).
3158 [ur,3145,500,2324,3117] 
          -member(pair(intersection(n$($c2,$c1),
          $c2),intersection(n$($c2,$c1),$c1)),cart(P($c2),P($c1))).
3165 [ur,3149,646,94] member(intersection(n$($c2,$c1),$c1),P($c1)).
3177 [ur,3158,14,3154] -member(intersection(n$($c2,$c1),$c1),P($c1)).
3178 [binary,3177.1,3165.1] $F.

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

clauses generated   38921
Kbytes malloced      2299
user CPU time           9.12  seconds