----- SUMMARY FOR THEOREM CUP-K-IM IN DIRECTORY Q:\cup ----- % CUP-K-IM.IN 2000 May 17 % Relating images of CUP and K formula_list(sos). % negation of Theorem CUP-K-IM -(all x subclass(image(CUP,cart(x,R(SINGLETON))),union(x,image(K,x)))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Thu May 18 11:14:56 2000 Length of proof is 23. Level of proof is 8. ---------------- 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). 14 [] member(pair(u,v),cart(x,y)) | -member(u,x) | -member(v,y). 15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x). 122 [] -member(x,union(y,z)) | member(x,y) | member(x,z). 123 [] -member(x,y) | member(x,union(y,z)). 124 [] -member(x,y) | member(x,union(z,y)). 292 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)). 301 [] -member(x,cart(y,z)) | member(first(x),y). 302 [] -member(x,cart(y,z)) | member(second(x),z). 384 [] -member(x,y) | -member(x,cart(V,V)) | member(first(x),D(y)). 481 [] subclass(image(x,y),R(x)). 494 [] -member(x,image(y,z)) | member(dom(y,z,x),z). 498 [] -member(x,y) | -member(pair(x,z),u) | -member(pair(x,z),cart(V,V)) | member(z,image(u,y)). 506 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),y). 526 [] -member(x,image(y,z)) | member(dom(y,z,x),D(y)). 916 [] -member(pair(x,y),Id) | equal(x,y). 1540 [] -member(pair(x,y),cart(V,R(SINGLETON))) | member(pair(x,union(x,y)),union(Id,K)). 2290 [] -member(pair(x,y),CUP) | equal(union(first(x),second(x)),y). 2304 [] -subclass(image(CUP,cart($c1,R(SINGLETON))), union($c1,image(K,$c1))). 2390 [] equal(D(cart(x,x)),x). 3077 [] equal(D(CUP),cart(V,V)). 3078 [] equal(R(CUP),V). 3079 [] equal(notsub(image(CUP,cart(x,R(SINGLETON))), union(x,image(K,x))),n$(x)). 3080 [] equal(dom(CUP,cart(x,R(SINGLETON)),n$(x)),d$(x)). 3081 [binary,2304.1,3.2,demod,3079] -member(n$($c1),union($c1,image(K,$c1))). 3082 [binary,2304.1,2.2,demod,3079] member(n$($c1),image(CUP,cart($c1,R(SINGLETON)))). 3084 [binary,3081.1,124.2] -member(n$($c1),image(K,$c1)). 3085 [binary,3081.1,123.2] -member(n$($c1),$c1). 3086 [binary,3082.1,526.1,demod,3080,3077] member(d$($c1),cart(V,V)). 3087 [binary,3082.1,506.1,demod,3080] member(pair(d$($c1),n$($c1)),CUP). 3089 [binary,3082.1,494.1,demod,3080] member(d$($c1),cart($c1,R(SINGLETON))). 3108 [ur,3082,1,481,demod,3078] member(n$($c1),V). 3115 [binary,3086.1,384.1,demod,2390,unit_del,3086] member(first(d$($c1)),V). 3117,3116 [binary,3086.1,15.1] equal(pair(first(d$($c1)),second(d$($c1))),d$($c1)). 3136,3135 [binary,3087.1,2290.1,flip.1] equal(n$($c1),union(first(d$($c1)),second(d$($c1)))). 3138 [back_demod,3108,demod,3136] member(union(first(d$($c1)),second(d$($c1))),V). 3159 [back_demod,3085,demod,3136] -member(union(first(d$($c1)),second(d$($c1))),$c1). 3160 [back_demod,3084,demod,3136] -member(union(first(d$($c1)),second(d$($c1))), image(K,$c1)). 3163 [binary,3089.1,302.1] member(second(d$($c1)),R(SINGLETON)). 3164 [binary,3089.1,301.1] member(first(d$($c1)),$c1). 3223 [para_from,3116.1.1,1540.1.1] -member(d$($c1),cart(V,R(SINGLETON))) | member(pair(first(d$($c1)),union(first(d$($c1)), second(d$($c1)))),union(Id,K)). 3290 [ur,3138,292,3115] member(pair(first(d$($c1)),union(first(d$($c1)), second(d$($c1)))),cart(V,V)). 3391 [ur,3163,14,3115,demod,3117] member(d$($c1),cart(V,R(SINGLETON))). 3572 [binary,3223.2,122.1,unit_del,3391] member(pair(first(d$($c1)),union(first(d$($c1)), second(d$($c1)))),Id) | member(pair(first(d$($c1)), union(first(d$($c1)),second(d$($c1)))),K). 3625 [ur,3290,498,3164,3160] -member(pair(first(d$($c1)),union(first(d$($c1)), second(d$($c1)))),K). 3864,3863 [binary,3572.1,916.1,unit_del,3625,flip.1] equal(union(first(d$($c1)),second(d$($c1))), first(d$($c1))). 3871 [back_demod,3159,demod,3864] -member(first(d$($c1)),$c1). 3872 [binary,3871.1,3164.1] $F. ------------ end of proof ------------- clauses generated 359363 Kbytes malloced 2554 user CPU time 57.94 seconds