----- SUMMARY FOR THEOREM H-TC-2 IN DIRECTORY Q:\h -----

% H-TC-2.IN                 2001 April 6
% This was discovered using the GOEDEL program

formula_list(sos).
% negation of Theorem H-TC-2
-(all x equal(image(inverse(TC),P(x)),P(H(x)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Apr 06 18:11:14 2001

Length of proof is 9. Level of proof is 5.

---------------- 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).
5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
76 [] subclass(x,x).
660 [] -member(x,P(y)) | subclass(x,y).
661 [] -member(x,V) | -subclass(x,y) | member(x,P(y)).
692 [] -subclass(U(x),y) | subclass(x,P(y)).
922 [] subclass(x,image(S,x)).
3709 [] -member(tc(x),y) | member(x,image(inverse(TC),y)).
3710 [] -member(x,image(inverse(TC),y)) | member(tc(x),y).
3732 [] -subclass(x,H(y)) | subclass(tc(x),y).
3733 [] -equal(image(inverse(TC),P($c1)),P(H($c1))).
3833 [] equal(R(inverse(x)),D(x)).
3849 [] equal(image(x,V),R(x)).
3977 [] equal(image(S,P(x)),V).
4911 [] equal(D(TC),V).
4920 [] equal(U(image(inverse(TC),x)),U(intersection(FULL,x))).
4921 [] equal(U(intersection(FULL,P(x))),H(x)).
4928 [] equal(notsub(P(H(x)),image(inverse(TC),P(x))),n$(x)).
4929 [binary,3733.1,5.3] 
          -subclass(image(inverse(TC),P($c1)),P(H($c1)))
           | -subclass(P(H($c1)),image(inverse(TC),P($c1))).
4930 [binary,4929.1,692.2,demod,4920,4921,unit_del,76] 
          -subclass(P(H($c1)),image(inverse(TC),P($c1))).
4936 [binary,4930.1,3.2,demod,4928] 
          -member(n$($c1),image(inverse(TC),P($c1))).
4937 [binary,4930.1,2.2,demod,4928] member(n$($c1),P(H($c1))).
4941 [binary,4936.1,3709.2] -member(tc(n$($c1)),P($c1)).
4943 [binary,4937.1,660.1] subclass(n$($c1),H($c1)).
4945 [ur,4937,1,922,demod,3977] member(n$($c1),V).
4948 [binary,4941.1,661.3] 
          -member(tc(n$($c1)),V) | -subclass(tc(n$($c1)),$c1).
4950 [binary,4943.1,3732.1] subclass(tc(n$($c1)),$c1).
4970 [binary,4948.1,3710.2,demod,3849,3833,4911,unit_del,4950,4945] 
          $F.

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

clauses generated   14536
Kbytes malloced      3512
user CPU time           4.51  seconds