----- SUMMARY FOR THEOREM DK-MEM-2 IN DIRECTORY Q:\dedekind -----

% DK-MEM-2.IN                 2000 June 12

formula_list(sos).
% negation of Theorem DK-MEM-2
-(all x y ((member(x,DEDEKIND) & member(pair(x,y),Q) & subclass(y,x))
           -> equal(x,y))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Jun 12 11:09:40 2000

Length of proof is 7. Level of proof is 3.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
4 [] subclass(x,V).
22 [] -member(x,complement(y)) | -member(x,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).
3307 [] member($c2,DEDEKIND).
3308 [] member(pair($c2,$c1),Q).
3309 [] subclass($c1,$c2).
3310 [] -equal($c2,$c1).
4217 [] equal(composite(PS,Q),composite(Q,PS)).
4369 [] equal(fix(composite(Q,PS)),complement(DEDEKIND)).
4370 [binary,3307.1,22.2] -member($c2,complement(DEDEKIND)).
4372 [ur,3307,1,4] member($c2,V).
4376 [binary,3308.1,1459.2,unit_del,2725] member(pair($c1,$c2),Q).
4378 [ur,3308,1,2679] member(pair($c2,$c1),cart(V,V)).
4380 [binary,3309.1,1677.2,unit_del,4372,3310] 
          member(pair($c1,$c2),PS).
4396 [ur,4376,1,2679] member(pair($c1,$c2),cart(V,V)).
4425 [ur,4396,753,3308,4378,4380,demod,4217] 
          member(pair($c2,$c2),composite(Q,PS)).
4458 [binary,4425.1,1175.2,demod,4369,unit_del,4372,4370] $F.

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

clauses generated   90923
Kbytes malloced      3033
user CPU time          13.02  seconds