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

% CUP-PC-1.IN                 2000 July 20

formula_list(sos).
% negation of Lemma CUP-PC-1
-(all x y subclass(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:22:34 2000

Length of proof is 18. Level of proof is 7.

---------------- 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).
4 [] subclass(x,V).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
127 [] equal(union(x,union(y,z)),union(y,union(x,z))).
142 [] subclass(x,union(x,y)).
143 [] subclass(x,union(y,x)).
144 [] -subclass(x,y) | -subclass(z,y) | subclass(union(x,z),y).
145 [] -subclass(x,y) | subclass(union(x,z),union(y,z)).
246 [] -member(x,V) | -subclass(singleton(x),y) | member(x,y).
301 [] -member(x,cart(y,z)) | member(first(x),y).
302 [] -member(x,cart(y,z)) | member(second(x),z).
494 [] -member(x,image(y,z)) | member(dom(y,z,x),z).
506 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),y).
645 [] -member(x,P(y)) | subclass(x,y).
646 [] -member(x,V) | -subclass(x,y) | member(x,P(y)).
2329 [] -member(pair(x,y),CUP) | equal(union(first(x),second(x)),y).
2331 [] -subclass(image(CUP,cart(P($c2),P($c1))),P(union($c2,$c1))).
2370 [] equal(union(union(x,y),z),union(x,union(y,z))).
3113 [] equal(notsub(image(CUP,cart(P(x),P(y))),
          P(union(x,y))),n$(x,y)).
3114 [] equal(dom(CUP,cart(P(x),P(y)),n$(x,y)),d$(x,y)).
3115 [] equal(first(d$(x,y)),f$(x,y)).
3116 [] equal(second(d$(x,y)),s$(x,y)).
3117 [binary,2331.1,3.2,demod,3113] 
          -member(n$($c2,$c1),P(union($c2,$c1))).
3118 [binary,2331.1,2.2,demod,3113] 
          member(n$($c2,$c1),image(CUP,cart(P($c2),P($c1)))).
3120 [binary,3117.1,646.3] 
          -member(n$($c2,$c1),V) | -subclass(n$($c2,$c1),
          union($c2,$c1)).
3125 [binary,3118.1,506.1,demod,3114] 
          member(pair(d$($c2,$c1),n$($c2,$c1)),CUP).
3126 [binary,3118.1,494.1,demod,3114] 
          member(d$($c2,$c1),cart(P($c2),P($c1))).
3129 [ur,3118,1,4] member(n$($c2,$c1),V).
3134 [binary,3120.1,246.3,unit_del,3129,4] 
          -subclass(n$($c2,$c1),union($c2,$c1)).
3148,3147 [binary,3125.1,2329.1,demod,3115,3116,flip.1] 
          equal(n$($c2,$c1),union(f$($c2,$c1),s$($c2,$c1))).
3154 [back_demod,3134,demod,3148] 
          -subclass(union(f$($c2,$c1),s$($c2,$c1)),union($c2,$c1)).
3161 [binary,3126.1,302.1,demod,3116] member(s$($c2,$c1),P($c1)).
3162 [binary,3126.1,301.1,demod,3115] member(f$($c2,$c1),P($c2)).
3187 [ur,3154,77,142,demod,2370] 
          -subclass(union(f$($c2,$c1),union(s$($c2,$c1),x)),
          union($c2,$c1)).
3206 [binary,3161.1,645.1] subclass(s$($c2,$c1),$c1).
3213 [binary,3162.1,645.1] subclass(f$($c2,$c1),$c2).
3277 [para_into,3187.1.1,127.1.2] 
          -subclass(union(s$($c2,$c1),union(f$($c2,$c1),x)),
          union($c2,$c1)).
3333 [ur,3206,77,143] subclass(s$($c2,$c1),union(x,$c1)).
3352 [binary,3213.1,145.1] 
          subclass(union(f$($c2,$c1),x),union($c2,x)).
3523 [binary,3277.1,144.3,unit_del,3333] 
          -subclass(union(f$($c2,$c1),x),union($c2,$c1)).
3524 [binary,3523.1,3352.1] $F.

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

clauses generated   73733
Kbytes malloced      2458
user CPU time          10.27  seconds