----- SUMMARY FOR THEOREM DK-MEM-1 IN DIRECTORY Q:\dedekind ----- % DK-MEM-1.IN 2000 June 12 formula_list(sos). % negation of Theorem DK-MEM-1 -(all x y ((member(x,DEDEKIND) & member(pair(x,y),Q) & subclass(x,y)) -> equal(x,y))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Mon Jun 12 11:09:26 2000 Length of proof is 9. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -member(x,y) | -subclass(y,z) | member(x,z). 4 [] subclass(x,V). 181 [] -member(x,y) | -member(x,z) | -disjoint(y,z). 185 [] disjoint(complement(x),x). 500 [] -member(x,y) | -member(pair(x,z),u) | -subclass(u,cart(V,V)) | member(z,image(u,y)). 753 [] -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)). 1175 [] -member(x,V) | -member(pair(x,x),y) | member(x,fix(y)). 1459 [] -EQUIVALENCE(x) | -member(pair(y,z),x) | member(pair(z,y),x). 1677 [] -member(x,V) | -subclass(y,x) | equal(y,x) | member(pair(y,x),PS). 2679 [] subclass(Q,cart(V,V)). 2725 [] EQUIVALENCE(Q). 3306 [] member($c2,DEDEKIND). 3307 [] member(pair($c2,$c1),Q). 3308 [] subclass($c2,$c1). 3309 [] -equal($c2,$c1). 3425 [] equal(image(x,V),R(x)). 4205 [] equal(R(Q),V). 4368 [] equal(fix(composite(Q,PS)),complement(DEDEKIND)). 4370 [ur,3306,181,185] -member($c2,complement(DEDEKIND)). 4371 [ur,3306,1,4] member($c2,V). 4374 [ur,3307,1459,2725] member(pair($c1,$c2),Q). 4376 [ur,3307,1,2679] member(pair($c2,$c1),cart(V,V)). 4384 [ur,4371,500,3307,2679,demod,3425,4205] member($c1,V). 4390 [ur,4374,1,2679] member(pair($c1,$c2),cart(V,V)). 4401 [ur,4384,1677,3308,3309] member(pair($c2,$c1),PS). 4416 [ur,4401,753,4376,4374,4390] member(pair($c2,$c2),composite(Q,PS)). 4429 [ur,4416,1175,4371,demod,4368] member($c2,complement(DEDEKIND)). 4430 [binary,4429.1,4370.1] $F. ------------ end of proof ------------- clauses generated 71758 Kbytes malloced 3033 user CPU time 11.15 seconds