----- SUMMARY FOR THEOREM H-I IN DIRECTORY Q:\h -----

% H-I.IN                 2001 March 24

formula_list(sos).
% negation of Theorem H-I
-(all x y equal(H(intersection(x,y)),intersection(H(x),H(y)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Mar 24 20:59:56 2001

Length of proof is 8. Level of proof is 8.

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

5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
93 [] subclass(intersection(x,y),x).
94 [] subclass(intersection(x,y),y).
95 [] -subclass(x,y) | -subclass(x,z) | subclass(x,
          intersection(y,z)).
3729 [] -subclass(x,H(y)) | subclass(tc(x),y).
3731 [] -subclass(x,y) | subclass(H(x),H(y)).
3736 [] -subclass(tc(x),y) | subclass(x,H(y)).
3737 [] -equal(H(intersection($c2,$c1)),intersection(H($c2),H($c1))).
4934 [binary,3737.1,5.3] 
          -subclass(H(intersection($c2,$c1)),
          intersection(H($c2),H($c1))) | -subclass(intersection(H($c2),
          H($c1)),H(intersection($c2,$c1))).
4935 [binary,4934.1,95.3] 
          -subclass(intersection(H($c2),H($c1)),
          H(intersection($c2,$c1))) | -subclass(H(intersection($c2,$c1)),
          H($c2)) | -subclass(H(intersection($c2,$c1)),H($c1)).
4937 [binary,4935.1,3736.2] 
          -subclass(H(intersection($c2,$c1)),H($c2))
           | -subclass(H(intersection($c2,$c1)),H($c1))
           | -subclass(tc(intersection(H($c2),H($c1))),
          intersection($c2,$c1)).
4943 [binary,4937.1,3731.2,unit_del,93] 
          -subclass(H(intersection($c2,$c1)),H($c1))
           | -subclass(tc(intersection(H($c2),H($c1))),
          intersection($c2,$c1)).
4949 [binary,4943.1,3731.2,unit_del,94] 
          -subclass(tc(intersection(H($c2),H($c1))),
          intersection($c2,$c1)).
4955 [binary,4949.1,95.3] 
          -subclass(tc(intersection(H($c2),H($c1))),$c2)
           | -subclass(tc(intersection(H($c2),H($c1))),$c1).
4965 [binary,4955.1,3729.2,unit_del,93] 
          -subclass(tc(intersection(H($c2),H($c1))),$c1).
4983 [binary,4965.1,3729.2] 
          -subclass(intersection(H($c2),H($c1)),H($c1)).
4984 [binary,4983.1,94.1] $F.

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

clauses generated    3504
Kbytes malloced      3033
user CPU time           3.52  seconds