----- SUMMARY FOR THEOREM GT-UB-U IN DIRECTORY Q:\greatest -----

% GT-UB-U.IN                 2000 December 20
% This theorem is not deep, but its proof requires a fairly high 
% max_weight, binary resolution, and a clause with three literals.

formula_list(sos).
% negation of Theorem GT-UB-U
-(all u v w x ((member(pair(u,w),UB(x)) & member(pair(v,w),GREATEST(x)))
               -> member(pair(union(u,v),w),GREATEST(x)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Wed Dec 20 14:20:59 2000

Length of proof is 10. Level of proof is 3.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
76 [] subclass(x,x).
126 [] -member(x,y) | member(x,union(z,y)).
146 [] -subclass(x,y) | -subclass(z,y) | subclass(union(x,z),y).
421 [] -member(pair(x,y),z) | -subclass(z,cart(V,V))
           | member(pair(y,x),inverse(z)).
614 [] -member(pair(x,y),cart(V,V)) | member(union(x,y),V).
773 [] -member(pair(x,y),z) | -member(pair(x,y),cart(V,V))
           | -member(pair(y,u),v) | -member(pair(y,u),cart(V,V))
           | member(pair(x,u),composite(v,z)).
1044 [] subclass(UB(x),cart(V,V)).
1048 [] -member(pair(x,y),UB(z)) | subclass(cart(x,singleton(y)),z).
1478 [] subclass(GREATEST(x),cart(V,V)).
1486 [] -member(pair(x,y),GREATEST(z)) | subclass(cart(x,singleton(y)),
          z).
1487 [] -member(pair(x,y),GREATEST(z)) | member(y,x).
1488 [] -member(x,V) | -member(y,x) | -subclass(cart(x,singleton(y)),
          z) | member(pair(x,y),GREATEST(z)).
1489 [] member(pair($c4,$c2),UB($c1)).
1490 [] member(pair($c3,$c2),GREATEST($c1)).
1491 [] -member(pair(union($c4,$c3),$c2),GREATEST($c1)).
1554 [] equal(cart(union(x,y),z),union(cart(x,z),cart(y,z))).
1592 [] equal(inverse(cart(x,y)),cart(y,x)).
1600 [] equal(R(cart(x,x)),x).
1609 [] equal(image(x,V),R(x)).
1712 [] equal(composite(x,cart(y,z)),cart(y,image(x,z))).
1926 [binary,1489.1,1048.1] subclass(cart($c4,singleton($c2)),$c1).
1927 [ur,1489,1,1044] member(pair($c4,$c2),cart(V,V)).
1928 [binary,1490.1,1487.1] member($c2,$c3).
1929 [binary,1490.1,1486.1] subclass(cart($c3,singleton($c2)),$c1).
1930 [ur,1490,1,1478] member(pair($c3,$c2),cart(V,V)).
1931 [binary,1491.1,1488.4,demod,1554] 
          -member(union($c4,$c3),V) | -member($c2,union($c4,$c3))
           | -subclass(union(cart($c4,singleton($c2)),
          cart($c3,singleton($c2))),$c1).
1956 [ur,1929,146,1926] 
          subclass(union(cart($c4,singleton($c2)),
          cart($c3,singleton($c2))),$c1).
1962 [binary,1930.1,421.1,demod,1592,unit_del,76] 
          member(pair($c2,$c3),cart(V,V)).
1969 [binary,1931.1,614.2,unit_del,1956] 
          -member($c2,union($c4,$c3)) | -member(pair($c4,$c3),
          cart(V,V)).
2088 [ur,1962,773,1927,1927,1962,demod,1712,1609,1600] 
          member(pair($c4,$c3),cart(V,V)).
2107 [binary,1969.1,126.2,unit_del,2088,1928] $F.

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

clauses generated   17963
Kbytes malloced      1628
user CPU time           3.68  seconds