----- SUMMARY FOR THEOREM FS-4 IN DIRECTORY Q:\FS -----

% FS-4.IN     1997 June 8

formula_list(sos).
% negation of Theorem FS-4
-(all x (member(x,FUNS) -> 
         -member(x,fix(composite(E,
      composite(cross(Id,complement(Id)),inverse(E))))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Jul 03 22:02:17 1997

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

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

23 [] -member(z,intersection(x,y)) | member(z,y).
26 [] -member(z,complement(x)) | -member(z,x).
731 [] equal(intersection(P(cart(V,V)),complement(fix(composite(E,
          composite(cross(Id,complement(Id)),inverse(E)))))),FUNS).
735 [] member($c1,FUNS).
736 [] member($c1,fix(composite(E,composite(cross(Id,complement(Id)),
          inverse(E))))).
839 [para_into,735.1.2,731.1.2] 
          member($c1,intersection(P(cart(V,V)),
          complement(fix(composite(E,composite(cross(Id,complement(Id)),
          inverse(E))))))).
840 [ur,736,26] -member($c1,complement(fix(composite(E,
          composite(cross(Id,complement(Id)),inverse(E)))))).
859 [ur,839,23] member($c1,complement(fix(composite(E,
          composite(cross(Id,complement(Id)),inverse(E)))))).
860 [binary,859.1,840.1] $F.

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

clauses generated     574
Kbytes malloced       670
user CPU time           1.65  seconds