----- SUMMARY FOR THEOREM GLB-FU-2 IN DIRECTORY Q:\glb -----

% GLB-FU-2.IN                 2000 November 25

formula_list(sos).
% negation of Theorem GLB-FU-2
-(all x (subclass(intersection(x,inverse(x)),Id) -> FUNCTION(GLB(x)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Nov 25 15:36:00 2000

Length of proof is 4. Level of proof is 3.

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

63 [] -subclass(composite(x,inverse(x)),Id)
           | -subclass(x,cart(V,V)) | FUNCTION(x).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
95 [] -subclass(x,y) | -subclass(x,z) | subclass(x,
          intersection(y,z)).
423 [] -subclass(x,y) | subclass(inverse(x),inverse(y)).
1491 [] subclass(GLB(x),cart(V,V)).
1492 [] subclass(composite(GLB(x),inverse(GLB(x))),x).
1493 [] subclass(intersection($c1,inverse($c1)),Id).
1494 [] -FUNCTION(GLB($c1)).
1708 [] equal(inverse(composite(x,y)),composite(inverse(y),
          inverse(x))).
1717 [] equal(composite(composite(x,y),z),
          composite(x,composite(y,z))).
1770 [] equal(inverse(inverse(x)),composite(Id,x)).
1778 [] equal(composite(Id,composite(x,y)),composite(x,y)).
1942 [binary,1493.1,77.2] 
          -subclass(x,intersection($c1,inverse($c1)))
           | subclass(x,Id).
1962 [binary,1494.1,63.3,unit_del,1491] 
          -subclass(composite(GLB($c1),inverse(GLB($c1))),Id).
1999 [binary,1942.1,95.3] 
          subclass(x,Id) | -subclass(x,$c1)
           | -subclass(x,inverse($c1)).
2200 [binary,1999.3,423.2] 
          subclass(inverse(x),Id) | -subclass(inverse(x),$c1)
           | -subclass(x,$c1).
2695 [binary,2200.3,1492.1,demod,1708,1770,
          1717,1778,1708,1770,1717,1778,unit_del,1962,1492] $F.

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

clauses generated   54333
Kbytes malloced      1852
user CPU time           7.96  seconds