----- SUMMARY FOR THEOREM DK-PIG IN DIRECTORY Q:\dedekind -----

% DK-PIG.IN                 2000 June 3
% Pigeonhole Principle

formula_list(sos).
% negation of Theorem DK-PIG
-(all x ((ONEONE(x) & subclass(R(x),D(x)) & member(D(x),DEDEKIND))
          -> equal(R(x),D(x)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Jun 03 12:31:09 2000

Length of proof is 10. Level of proof is 5.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
4 [] subclass(x,V).
76 [] subclass(x,x).
181 [] -member(x,y) | -member(x,z) | -disjoint(y,z).
185 [] disjoint(complement(x),x).
292 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
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)).
1322 [] -member(x,y) | -subclass(z,x) | member(z,image(inverse(S),
          y)).
1669 [] subclass(PS,cart(V,V)).
1674 [] -member(x,V) | -subclass(y,x) | equal(y,x)
           | member(pair(y,x),PS).
2648 [] -ONEONE(x) | -member(D(x),V) | member(x,BIJ).
2671 [] -member(x,BIJ) | -subclass(y,D(x))
           | member(pair(y,image(x,y)),Q).
3285 [] ONEONE($c1).
3286 [] subclass(R($c1),D($c1)).
3287 [] member(D($c1),DEDEKIND).
3288 [] -equal(R($c1),D($c1)).
3389 [] equal(R(inverse(x)),D(x)).
3403 [] equal(image(x,D(x)),R(x)).
3404 [] equal(image(x,V),R(x)).
3525 [] equal(D(S),V).
4191 [] equal(composite(PS,Q),composite(Q,PS)).
4343 [] equal(fix(composite(Q,PS)),complement(DEDEKIND)).
4346 [ur,3287,181,185] -member(D($c1),complement(DEDEKIND)).
4347 [ur,3287,1,4] member(D($c1),V).
4348 [ur,4347,2648,3285] member($c1,BIJ).
4349 [ur,4347,1674,3286,3288] member(pair(R($c1),D($c1)),PS).
4351 [ur,4347,1322,3286,demod,3404,3389,3525] member(R($c1),V).
4352 [ur,4348,2671,76,demod,3403] member(pair(D($c1),R($c1)),Q).
4358 [ur,4349,1,1669] member(pair(R($c1),D($c1)),cart(V,V)).
4366 [ur,4351,292,4347] member(pair(D($c1),R($c1)),cart(V,V)).
4384 [ur,4366,753,4352,4349,4358,demod,4191] 
          member(pair(D($c1),D($c1)),composite(Q,PS)).
4396 [ur,4384,1175,4347,demod,4343] 
          member(D($c1),complement(DEDEKIND)).
4397 [binary,4396.1,4346.1] $F.

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

clauses generated   72463
Kbytes malloced      3033
user CPU time          12.69  seconds