----- SUMMARY FOR THEOREM HC-A-3 IN DIRECTORY Q:\HC -----

% HC-A-3.IN                 2001 April 14
% This theorem was discovered using the GOEDEL program.

formula_list(sos).
% negation of Theorem HC-A-3
-(all x equal(H(A(x)),A(image(HC,x)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Apr 14 14:12:47 2001

Length of proof is 12. Level of proof is 6.

---------------- 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).
4 [] subclass(x,V).
5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
505 [] -member(x,image(y,z)) | member(dom(y,z,x),z).
518 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),y).
632 [] -member(x,y) | subclass(A(y),x).
636 [] -member(x,ran(complement(E),x,y)) | member(x,A(y)).
637 [] -member(x,V) | member(x,A(y)) | member(ran(complement(E),
          x,y),y).
3734 [] -subclass(x,y) | subclass(H(x),H(y)).
3752 [] -member(pair(x,y),HC) | equal(y,H(x)).
3754 [] subclass(A(image(HC,x)),H(A(x))).
3755 [] -equal(H(A($c1)),A(image(HC,$c1))).
4959 [] equal(notsub(H(A(x)),A(image(HC,x))),n$(x)).
4960 [] equal(ran(complement(E),n$(x),image(HC,x)),r$(x)).
4961 [] equal(dom(HC,x,r$(x)),d$(x)).
4962 [binary,3755.1,5.3,unit_del,3754] 
          -subclass(H(A($c1)),A(image(HC,$c1))).
4964 [binary,4962.1,3.2,demod,4959] 
          -member(n$($c1),A(image(HC,$c1))).
4965 [binary,4962.1,2.2,demod,4959] member(n$($c1),H(A($c1))).
4969 [binary,4964.1,637.2,demod,4960] 
          -member(n$($c1),V) | member(r$($c1),image(HC,$c1)).
4970 [binary,4964.1,636.2,demod,4960] -member(n$($c1),r$($c1)).
4977 [ur,4965,1,4] member(n$($c1),V).
4988 [binary,4969.2,518.1,demod,4961,unit_del,4977] 
          member(pair(d$($c1),r$($c1)),HC).
4990 [binary,4969.2,505.1,demod,4961,unit_del,4977] 
          member(d$($c1),$c1).
4992 [ur,4970,1,4965] -subclass(H(A($c1)),r$($c1)).
5035,5034 [binary,4988.1,3752.1,flip.1] equal(H(d$($c1)),r$($c1)).
5042 [binary,4990.1,632.1] subclass(A($c1),d$($c1)).
5183 [binary,5042.1,3734.1,demod,5035] subclass(H(A($c1)),r$($c1)).
5184 [binary,5183.1,4992.1] $F.

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

clauses generated  147902
Kbytes malloced      3608
user CPU time          20.82  seconds