----- SUMMARY FOR THEOREM FS-PC-3 IN DIRECTORY Q:\fs ----- % FS-PC-3.IN 2000 February 10 formula_list(sos). % negation of Corollary FS-PC-3 -(all x (FUNCTION(U(x)) -> subclass(x,FUNS))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Thu Feb 10 21:21:42 2000 Length of proof is 2. Level of proof is 1. ---------------- PROOF ---------------- 77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z). 585 [] subclass(x,P(U(x))). 2172 [] -FUNCTION(x) | subclass(P(x),FUNS). 2174 [] FUNCTION(U($c1)). 2175 [] -subclass($c1,FUNS). 2943 [ur,2174,2172] subclass(P(U($c1)),FUNS). 3008 [ur,2175,77,585] -subclass(P(U($c1)),FUNS). 3009 [binary,3008.1,2943.1] $F. ------------ end of proof ------------- clauses generated 333 Kbytes malloced 2139 user CPU time 1.64 seconds