----- SUMMARY FOR THEOREM H-A IN DIRECTORY Q:\H -----

% H-A.IN                 2001 April 19
% Statement of HC-A-1 with quantifiers in Otter notation.

formula_list(sos).
% negation of Corollary H-A
-(all x y z ((member(x,H(A(y))) & member(z,y)) -> member(x,H(z)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Apr 19 22:33:53 2001

Length of proof is 3. Level of proof is 2.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
632 [] -member(x,y) | subclass(A(y),x).
3734 [] -subclass(x,y) | subclass(H(x),H(y)).
3735 [] member($c3,H(A($c2))).
3736 [] member($c1,$c2).
3737 [] -member($c3,H($c1)).
4936 [ur,3736,632] subclass(A($c2),$c1).
4940 [ur,3737,1,3735] -subclass(H(A($c2)),H($c1)).
4950 [ur,4936,3734] subclass(H(A($c2)),H($c1)).
4951 [binary,4950.1,4940.1] $F.

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

clauses generated   16867
Kbytes malloced      3512
user CPU time           4.17  seconds