----- SUMMARY FOR THEOREM DK-K IN DIRECTORY Q:\dedekind ----- % DK-K.IN 2000 June 2 formula_list(sos). % negation of Theorem DK-K -subclass(image(K,DEDEKIND),DEDEKIND). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Fri Jun 02 20:24:08 2000 Length of proof is 26. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -member(x,y) | -subclass(y,z) | member(x,z). 2 [] member(notsub(x,y),x) | subclass(x,y). 22 [] -member(x,complement(y)) | -member(x,y). 110 [] member(notsub(x,y),complement(y)) | subclass(x,y). 292 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)). 413 [] -member(pair(x,y),inverse(z)) | member(pair(y,x),z). 415 [] -member(pair(x,y),z) | -subclass(z,cart(V,V)) | member(pair(y,x),inverse(z)). 494 [] -member(x,image(y,z)) | member(dom(y,z,x),z). 504 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),cart(V,V)). 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)). 731 [] subclass(composite(x,y),cart(V,V)). 745 [] -subclass(x,y) | subclass(composite(z,x),composite(z,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)). 788 [] -member(pair(x,y),composite(z,u)) | member(pair(x,com(z,u,x,y)),u). 789 [] -member(pair(x,y),composite(z,u)) | member(pair(x,com(z,u,x,y)),cart(V,V)). 790 [] -member(pair(x,y),composite(z,u)) | member(pair(com(z,u,x,y),y),z). 791 [] -member(pair(x,y),composite(z,u)) | member(pair(com(z,u,x,y),y),cart(V,V)). 1175 [] -member(x,V) | -member(pair(x,x),y) | member(x,fix(y)). 1176 [] -member(x,fix(y)) | member(pair(x,x),y). 1459 [] -EQUIVALENCE(x) | -member(pair(y,z),x) | -member(pair(z,u),x) | member(pair(y,u),x). 1472 [] EQUIVALENCE(cart(x,x)). 1689 [] subclass(K,cart(V,V)). 2694 [] subclass(composite(inverse(K),composite(K,x)), composite(Q,x)). 2716 [] equal(complement(fix(composite(Q,PS))),DEDEKIND). 2717 [] -subclass(image(K,DEDEKIND),DEDEKIND). 2749 [] equal(complement(complement(x)),x). 2929 [] equal(inverse(composite(x,y)),composite(inverse(y), inverse(x))). 2938 [] equal(composite(composite(x,y),z), composite(x,composite(y,z))). 3223 [] equal(composite(PS,K),composite(K,PS)). 3224 [] equal(D(K),V). 3614 [] equal(inverse(Q),Q). 3616 [] equal(composite(inverse(K),Q),composite(Q,inverse(K))). 3623 [] equal(composite(Q,Q),Q). 3626 [] equal(notsub(image(K,DEDEKIND),DEDEKIND),n$). 3627 [] equal(dom(K,DEDEKIND,n$),d$). 3628 [] equal(com(Q,PS,n$,n$),m$). 3629 [binary,2717.1,110.2,demod,3626] member(n$,complement(DEDEKIND)). 3632 [binary,2717.1,2.2,demod,3626] member(n$,image(K,DEDEKIND)). 3636 [para_into,3629.1.2.1,2716.1.2,demod,2749] member(n$,fix(composite(Q,PS))). 3640 [binary,3632.1,526.1,demod,3627,3224] member(d$,V). 3641 [binary,3632.1,506.1,demod,3627] member(pair(d$,n$),K). 3642 [binary,3632.1,504.1,demod,3627] member(pair(d$,n$),cart(V,V)). 3643 [binary,3632.1,494.1,demod,3627] member(d$,DEDEKIND). 3647 [binary,3636.1,1176.1] member(pair(n$,n$),composite(Q,PS)). 3652 [ur,3640,292,3636] member(pair(n$,d$),cart(V,V)). 3655 [binary,3641.1,415.1,unit_del,1689] member(pair(n$,d$),inverse(K)). 3658 [binary,3643.1,22.2] -member(d$,complement(DEDEKIND)). 3664 [binary,3647.1,791.1,demod,3628] member(pair(m$,n$),cart(V,V)). 3665 [binary,3647.1,790.1,demod,3628] member(pair(m$,n$),Q). 3666 [binary,3647.1,789.1,demod,3628] member(pair(n$,m$),cart(V,V)). 3667 [binary,3647.1,788.1,demod,3628] member(pair(n$,m$),PS). 3689 [para_into,3658.1.2.1,2716.1.2,demod,2749] -member(d$,fix(composite(Q,PS))). 3692 [ur,3664,1459,1472,3652] member(pair(m$,d$),cart(V,V)). 3696 [ur,3665,753,3664,3655,3652,demod,3616] member(pair(m$,d$),composite(Q,inverse(K))). 3698 [ur,3666,1459,1472,3642] member(pair(d$,m$),cart(V,V)). 3703 [ur,3667,753,3641,3642,3666,demod,3223] member(pair(d$,m$),composite(K,PS)). 3748 [binary,3689.1,1175.3,unit_del,3640] -member(pair(d$,d$),composite(Q,PS)). 3789 [ur,3703,753,3698,3696,3692,demod,2938] member(pair(d$,d$),composite(Q,composite(inverse(K), composite(K,PS)))). 3831 [binary,3748.1,413.2,demod,2929,3614] -member(pair(d$,d$),composite(inverse(PS),Q)). 3971 [binary,3789.1,1.1] -subclass(composite(Q,composite(inverse(K),composite(K,PS))), x) | member(pair(d$,d$),x). 4256 [binary,3971.1,745.2] member(pair(d$,d$),composite(Q,x)) | -subclass(composite(inverse(K),composite(K,PS)),x). 4613 [binary,4256.2,2694.1] member(pair(d$,d$),composite(Q,composite(Q,PS))). 5035 [binary,4613.1,415.1,demod,2929,2929, 3614,3614,2938,3623,unit_del,731,3831] $F. ------------ end of proof ------------- clauses generated 406468 Kbytes malloced 3193 user CPU time 71.35 seconds