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

% FS-5.IN     1997 June 8

formula_list(sos).
% negation of Theorem FS-5
-(all x ((member(x,FUNS) -> disjoint(cart(x,x),cross(Id,complement(Id)))))).
end_of_list.


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

Length of proof is 19. Level of proof is 5.

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

1 [] -subclass(x,y) | -member(u,x) | member(u,y).
4 [] subclass(x,V).
17 [] -member(z,cart(x,y)) | equal(z,pair(first(z),second(z))).
207 [] subclass(cart(x,y),cart(V,V)).
208 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
214 [] -member(z,cart(x,y)) | member(first(z),x).
215 [] -member(z,cart(x,y)) | member(second(z),y).
263 [] member(notsub(x,complement(y)),x) | disjoint(x,y).
264 [] member(notsub(x,complement(y)),y) | disjoint(x,y).
306 [] -member(pair(u,v),x) | -member(pair(u,v),cart(V,V))
           | member(pair(v,u),inverse(x)).
457 [] -member(pair(u,v),cart(V,V)) | -member(pair(v,w),cart(V,V))
           | -member(pair(u,v),y) | -member(pair(v,w),x)
           | member(pair(u,w),composite(x,y)).
488 [] -member(x,y) | -member(y,V) | member(pair(x,y),E).
612 [] -member(x,V) | -member(pair(x,x),y) | member(x,fix(y)).
738 [] -member(x,FUNS) | -member(x,fix(composite(E,
          composite(cross(Id,complement(Id)),inverse(E))))).
739 [] member($c1,FUNS).
740 [] -disjoint(cart($c1,$c1),cross(Id,complement(Id))).
840 [] equal(notsub(cart(x,x),complement(cross(Id,complement(Id)))),
          n$(x)).
841 [] equal(first(n$(x)),f$(x)).
842 [] equal(second(n$(x)),s$(x)).
843 [ur,739,738] -member($c1,fix(composite(E,
          composite(cross(Id,complement(Id)),inverse(E))))).
845 [ur,739,1,4] member($c1,V).
846 [ur,740,264,demod,840] member(n$($c1),cross(Id,complement(Id))).
847 [ur,740,263,demod,840] member(n$($c1),cart($c1,$c1)).
849 [ur,845,612,843] 
          -member(pair($c1,$c1),composite(E,
          composite(cross(Id,complement(Id)),inverse(E)))).
853 [ur,847,215,demod,842] member(s$($c1),$c1).
854 [ur,847,214,demod,841] member(f$($c1),$c1).
857,856 [ur,847,17,demod,841,842] 
          equal(n$($c1),pair(f$($c1),s$($c1))).
858 [ur,847,1,207,demod,857] member(pair(f$($c1),s$($c1)),cart(V,V)).
861 [back_demod,846,demod,857] 
          member(pair(f$($c1),s$($c1)),cross(Id,complement(Id))).
863 [ur,853,488,845] member(pair(s$($c1),$c1),E).
865 [ur,853,208,845] member(pair($c1,s$($c1)),cart(V,V)).
866 [ur,853,208,845] member(pair(s$($c1),$c1),cart(V,V)).
869 [ur,854,488,845] member(pair(f$($c1),$c1),E).
871 [ur,854,208,845] member(pair($c1,f$($c1)),cart(V,V)).
872 [ur,854,208,845] member(pair(f$($c1),$c1),cart(V,V)).
884 [ur,866,457,865,863,849] 
          -member(pair($c1,s$($c1)),composite(cross(Id,complement(Id)),
          inverse(E))).
896 [ur,872,306,869] member(pair($c1,f$($c1)),inverse(E)).
914 [ur,884,457,871,858,861] -member(pair($c1,f$($c1)),inverse(E)).
915 [binary,914.1,896.1] $F.

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

clauses generated    7871
Kbytes malloced       766
user CPU time           4.78  seconds